Skip to content

Commit a5d2118

Browse files
Add SMT2 FPA backend tests for fp.fma emission
Verify that --smt2 --fpa emits fp.fma (not bitvector encoding) for both normal FMA operations and special cases (NaN, infinity). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
1 parent 67f0ec6 commit a5d2118

2 files changed

Lines changed: 20 additions & 0 deletions

File tree

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE smt-backend
2+
precision.c
3+
--smt2 --fpa --outfile -
4+
fp\.fma
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
--
8+
^warning: ignoring
9+
--
10+
Verify that the SMT2 FPA backend emits fp.fma (not a bitvector encoding).
Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE smt-backend
2+
special_cases.c
3+
--smt2 --fpa --outfile -
4+
fp\.fma
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
--
8+
^warning: ignoring
9+
--
10+
Verify that FMA special cases (NaN, inf) emit fp.fma via FPA backend.

0 commit comments

Comments
 (0)