diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2019-04-04 12:31:21 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-04-04 12:31:21 -0500 |
| commit | a44c62c18a8380c089764decdd4c533268b4ef30 (patch) | |
| tree | e79af51595bc33ed0101b9552085173351b193e7 /test/regress/regress0/fp | |
| parent | ae712e32aae0947205f506f7caacc670311c6763 (diff) | |
Ignoring FP benchmarks with "unsafe" sizes unless option (#2931)
Diffstat (limited to 'test/regress/regress0/fp')
| -rw-r--r-- | test/regress/regress0/fp/abs-unsound.smt2 | 1 | ||||
| -rw-r--r-- | test/regress/regress0/fp/abs-unsound2.smt2 | 1 | ||||
| -rw-r--r-- | test/regress/regress0/fp/wrong-model.smt2 | 3 |
3 files changed, 4 insertions, 1 deletions
diff --git a/test/regress/regress0/fp/abs-unsound.smt2 b/test/regress/regress0/fp/abs-unsound.smt2 index 4ac53b830..b5aa0452e 100644 --- a/test/regress/regress0/fp/abs-unsound.smt2 +++ b/test/regress/regress0/fp/abs-unsound.smt2 @@ -1,4 +1,5 @@ ; REQUIRES: symfpu +; COMMAND-LINE: --fp-exp ; EXPECT: sat (set-logic QF_FP) (set-info :status sat) diff --git a/test/regress/regress0/fp/abs-unsound2.smt2 b/test/regress/regress0/fp/abs-unsound2.smt2 index a6172b157..ad603f8c9 100644 --- a/test/regress/regress0/fp/abs-unsound2.smt2 +++ b/test/regress/regress0/fp/abs-unsound2.smt2 @@ -1,4 +1,5 @@ ; REQUIRES: symfpu +; COMMAND-LINE: --fp-exp ; EXPECT: unsat (set-logic QF_FP) (set-info :status unsat) diff --git a/test/regress/regress0/fp/wrong-model.smt2 b/test/regress/regress0/fp/wrong-model.smt2 index 4bb7645d5..7694d8a35 100644 --- a/test/regress/regress0/fp/wrong-model.smt2 +++ b/test/regress/regress0/fp/wrong-model.smt2 @@ -1,10 +1,11 @@ ; REQUIRES: symfpu +; COMMAND-LINE: --fp-exp ; EXPECT: sat ; NOTE: the (set-logic ALL) is on purpose because the problem was not triggered ; with QF_FP. (set-logic ALL) -(declare-const r RoundingMode) +(declare-const r RoundingMode) (declare-const x (_ FloatingPoint 5 11)) (declare-const y (_ FloatingPoint 5 11)) (assert (not (= (fp.isSubnormal x) false))) |