diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2021-05-04 12:44:39 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2021-05-04 12:44:39 -0500 |
commit | a1df230df8d2ab08d6ce2bc69a707f730a8120ff (patch) | |
tree | b14b8d9a52c9c0918fea365530e963d2df0a41e8 /test/regress | |
parent | 178e201f3e47b95ae3e4912269ba19cd95e2dab3 (diff) | |
parent | 4f265b2c81c4cb858942f6e1e51ce8abdd01345b (diff) |
Merge branch 'master' of https://github.com/CVC4/CVC4 into proof-new
Diffstat (limited to 'test/regress')
-rw-r--r-- | test/regress/CMakeLists.txt | 6 | ||||
-rw-r--r-- | test/regress/regress0/fp/from_sbv.smt2 | 15 | ||||
-rw-r--r-- | test/regress/regress0/fp/from_ubv.smt2 | 5 | ||||
-rw-r--r-- | test/regress/regress0/fp/issue3582.smt2 | 7 | ||||
-rw-r--r-- | test/regress/regress0/fp/issue5511.smt2 | 6 | ||||
-rw-r--r-- | test/regress/regress0/fp/issue5734.smt2 | 7 | ||||
-rw-r--r-- | test/regress/regress0/fp/issue6164.smt2 | 7 |
7 files changed, 53 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 5a557a8a3..7e35487af 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -573,10 +573,16 @@ set(regress_0_tests regress0/fp/abs-unsound2.smt2 regress0/fp/down-cast-RNA.smt2 regress0/fp/ext-rew-test.smt2 + regress0/fp/from_ubv.smt2 + regress0/fp/from_sbv.smt2 regress0/fp/issue-5524.smt2 regress0/fp/issue3536.smt2 + regress0/fp/issue3582.smt2 regress0/fp/issue3619.smt2 regress0/fp/issue4277-assign-func.smt2 + regress0/fp/issue5511.smt2 + regress0/fp/issue5734.smt2 + regress0/fp/issue6164.smt2 regress0/fp/rti_3_5_bug.smt2 regress0/fp/simple.smt2 regress0/fp/wrong-model.smt2 diff --git a/test/regress/regress0/fp/from_sbv.smt2 b/test/regress/regress0/fp/from_sbv.smt2 new file mode 100644 index 000000000..226d6589c --- /dev/null +++ b/test/regress/regress0/fp/from_sbv.smt2 @@ -0,0 +1,15 @@ +; COMMAND-LINE: --fp-exp +; EXPECT: unsat +(set-logic QF_BVFP) +(declare-const x (_ BitVec 1)) +(declare-const rm RoundingMode) +(assert (or + (distinct ((_ to_fp 5 11) rm #b1) (fp #b1 #b01111 #b0000000000)) + (distinct ((_ to_fp 5 11) rm #b0) (_ +zero 5 11)) + (ite + (= x #b1) + (= ((_ to_fp 5 11) rm x) ((_ to_fp_unsigned 5 11) rm x)) + (distinct ((_ to_fp 5 11) rm x) ((_ to_fp_unsigned 5 11) rm x)) + ) + )) +(check-sat) diff --git a/test/regress/regress0/fp/from_ubv.smt2 b/test/regress/regress0/fp/from_ubv.smt2 new file mode 100644 index 000000000..6939e478a --- /dev/null +++ b/test/regress/regress0/fp/from_ubv.smt2 @@ -0,0 +1,5 @@ +; EXPECT: unsat +(set-logic QF_FP) +(declare-const r RoundingMode) +(assert (distinct ((_ to_fp_unsigned 8 24) r (_ bv0 1)) (fp (_ bv0 1) (_ bv0 8) (_ bv0 23)))) +(check-sat) diff --git a/test/regress/regress0/fp/issue3582.smt2 b/test/regress/regress0/fp/issue3582.smt2 new file mode 100644 index 000000000..2de76b680 --- /dev/null +++ b/test/regress/regress0/fp/issue3582.smt2 @@ -0,0 +1,7 @@ +; REQUIRES: symfpu +; EXPECT: unsat +(set-logic QF_FP) +(declare-fun bv () (_ BitVec 1)) +(define-fun x () (_ FloatingPoint 11 53) ((_ to_fp_unsigned 11 53) RNE bv)) +(assert (fp.isNaN x)) +(check-sat) diff --git a/test/regress/regress0/fp/issue5511.smt2 b/test/regress/regress0/fp/issue5511.smt2 new file mode 100644 index 000000000..d4393486c --- /dev/null +++ b/test/regress/regress0/fp/issue5511.smt2 @@ -0,0 +1,6 @@ +; REQUIRES: symfpu +; EXPECT: sat +(set-logic QF_FP) +(declare-fun a () (_ FloatingPoint 53 11)) +(assert (= a (_ +oo 53 11))) +(check-sat) diff --git a/test/regress/regress0/fp/issue5734.smt2 b/test/regress/regress0/fp/issue5734.smt2 new file mode 100644 index 000000000..2ad9ac921 --- /dev/null +++ b/test/regress/regress0/fp/issue5734.smt2 @@ -0,0 +1,7 @@ +; REQUIRES: symfpu +; EXPECT: sat +(set-logic QF_FP) +(declare-fun a () RoundingMode) +(declare-fun b () (_ FloatingPoint 8 24)) +(assert (= b (fp.add a b (fp.add a ((_ to_fp 8 24) a ((_ to_fp 8 24) a 0)) b)))) +(check-sat) diff --git a/test/regress/regress0/fp/issue6164.smt2 b/test/regress/regress0/fp/issue6164.smt2 new file mode 100644 index 000000000..056a98afc --- /dev/null +++ b/test/regress/regress0/fp/issue6164.smt2 @@ -0,0 +1,7 @@ +; REQUIRES: symfpu +; EXPECT: sat +; EXPECT: ((((_ to_fp 5 11) roundNearestTiesToAway (/ 1 10)) (fp #b0 #b01011 #b1001100110))) +(set-logic ALL) +(set-option :produce-models true) +(check-sat) +(get-value (((_ to_fp 5 11) RNA 0.1))) |