diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-01 12:22:09 -0500 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-08-01 10:22:09 -0700 |
| commit | 0aa6e039827750757941751e0829575a55601ace (patch) | |
| tree | 25e21dfd16e232e07615791935bfc6c32fc5bcab /test/regress | |
| parent | b721666fd7a2dafaaeb112059c2588c99e8020ec (diff) | |
Fix issues with bv2nat (#2219)
This includes:
- A missing case in the smt2 printer,
- A bug in an inference of int2bv applied to bv2nat where the types are different.
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/Makefile.tests | 1 | ||||
| -rw-r--r-- | test/regress/regress1/bv/bv2nat-types.smt2 | 7 |
2 files changed, 8 insertions, 0 deletions
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index c15e3d045..0b9e415fa 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1045,6 +1045,7 @@ REG1_TESTS = \ regress1/bv/bv-proof00.smt \ regress1/bv/bv2nat-ground.smt2 \ regress1/bv/bv2nat-simp-range-sat.smt2 \ + regress1/bv/bv2nat-types.smt2 \ regress1/bv/cmu-rdk-3.smt2 \ regress1/bv/decision-weight00.smt2 \ regress1/bv/divtest.smt2 \ diff --git a/test/regress/regress1/bv/bv2nat-types.smt2 b/test/regress/regress1/bv/bv2nat-types.smt2 new file mode 100644 index 000000000..e75ffb3ca --- /dev/null +++ b/test/regress/regress1/bv/bv2nat-types.smt2 @@ -0,0 +1,7 @@ +(set-logic QF_ALL) +(set-info :status sat) +(declare-fun x () (_ BitVec 8)) +(assert +(= (concat #b000000000000000000000000 x) ((_ int2bv 32) (bv2nat x))) +) +(check-sat) |