From a44c62c18a8380c089764decdd4c533268b4ef30 Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Thu, 4 Apr 2019 12:31:21 -0500 Subject: Ignoring FP benchmarks with "unsafe" sizes unless option (#2931) --- test/regress/regress0/fp/abs-unsound.smt2 | 1 + test/regress/regress0/fp/abs-unsound2.smt2 | 1 + test/regress/regress0/fp/wrong-model.smt2 | 3 ++- 3 files changed, 4 insertions(+), 1 deletion(-) (limited to 'test/regress') 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))) -- cgit v1.2.3