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 | |
parent | 448ee080458373fbd3aabe97396101d98d68f0c0 (diff) |
Fix unsound double abs rewrite rule for FP (#2792)
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/CMakeLists.txt | 2 | ||||
-rw-r--r-- | test/regress/regress0/fp/abs-unsound.smt2 | 11 | ||||
-rw-r--r-- | test/regress/regress0/fp/abs-unsound2.smt2 | 9 |
3 files changed, 22 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index e6e28336e..dbefe3af2 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -444,6 +444,8 @@ set(regress_0_tests regress0/fmf/sort-infer-typed-082718.smt2 regress0/fmf/syn002-si-real-int.smt2 regress0/fmf/tail_rec.smt2 + regress0/fp/abs-unsound.smt2 + regress0/fp/abs-unsound2.smt2 regress0/fp/ext-rew-test.smt2 regress0/fp/simple.smt2 regress0/fuzz_1.smt 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) |