diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-05-03 13:27:02 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-05-03 20:27:02 +0000 |
| commit | c8c7a075428e6193dee86e57a9ecb8af11af270c (patch) | |
| tree | ac12ea111a8228c594495573bc5407a05d3b3131 /test/regress | |
| parent | 439ab123cccdbf4f046b4e084ce996a1dc2aa758 (diff) | |
FP: Rewrite to_fp conversion from signed bit-vector. (#6472)
SymFPU does not allow to_fp conversion from signed bv of size 1. This
adds rewrites for this case.
Rewrites for the constant and the non-constant cases were tested in
isolation.
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/fp/from_sbv.smt2 | 15 |
2 files changed, 16 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 765b12e90..685ac8b4e 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -574,6 +574,7 @@ set(regress_0_tests 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 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) |