Skip to content

Commit 6756b84

Browse files
Add end-to-end SMT FPA test for FMA special cases
Run main_03.c (NaN, infinity, 0*inf) through an external SMT solver with --smt2 --fpa to verify the fp.fma emission produces correct verification results, not just correct syntax. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
1 parent a5d2118 commit 6756b84

1 file changed

Lines changed: 11 additions & 0 deletions

File tree

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE smt-backend
2+
special_cases.c
3+
--smt2 --fpa --no-built-in-assertions
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^warning: ignoring
9+
--
10+
Run FMA special cases through an external SMT solver with FPA theory.
11+
Verifies NaN, infinity, and 0*inf handling end-to-end.

0 commit comments

Comments
 (0)