diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-01-15 10:54:02 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-01-15 10:54:02 -0600 |
| commit | da504025a3a77e9a3201af33ee6f96f937802807 (patch) | |
| tree | cd23822d9806e5f0cc29fe871b0c1cf24a89921d /test/regress/regress0/fp | |
| parent | 448ee080458373fbd3aabe97396101d98d68f0c0 (diff) | |
Fix unsound double abs rewrite rule for FP (#2792)
Diffstat (limited to 'test/regress/regress0/fp')
| -rw-r--r-- | test/regress/regress0/fp/abs-unsound.smt2 | 11 | ||||
| -rw-r--r-- | test/regress/regress0/fp/abs-unsound2.smt2 | 9 |
2 files changed, 20 insertions, 0 deletions
diff --git a/test/regress/regress0/fp/abs-unsound.smt2 b/test/regress/regress0/fp/abs-unsound.smt2 new file mode 100644 index 000000000..4ac53b830 --- /dev/null +++ b/test/regress/regress0/fp/abs-unsound.smt2 @@ -0,0 +1,11 @@ +; REQUIRES: symfpu +; EXPECT: sat +(set-logic QF_FP) +(set-info :status sat) +(declare-fun x () (_ FloatingPoint 3 5)) +(declare-fun y () (_ FloatingPoint 3 5)) + +(assert (not (= (fp.abs (fp.abs x)) x))) +(assert (not (= (fp.abs (fp.neg y)) y))) + +(check-sat) diff --git a/test/regress/regress0/fp/abs-unsound2.smt2 b/test/regress/regress0/fp/abs-unsound2.smt2 new file mode 100644 index 000000000..a6172b157 --- /dev/null +++ b/test/regress/regress0/fp/abs-unsound2.smt2 @@ -0,0 +1,9 @@ +; REQUIRES: symfpu +; EXPECT: unsat +(set-logic QF_FP) +(set-info :status unsat) +(declare-fun x () (_ FloatingPoint 3 5)) + +(assert (fp.isNegative (fp.abs (fp.neg x)))) + +(check-sat) |