diff options
| author | Clark Barrett <barrett@cs.stanford.edu> | 2016-12-02 16:25:26 -0800 |
|---|---|---|
| committer | Clark Barrett <barrett@cs.stanford.edu> | 2016-12-02 16:28:17 -0800 |
| commit | c356e6b4e5aecd6d13e398b361eb15a4dea18d91 (patch) | |
| tree | 377b6ce7c65def72cadeb3d47319521b7c3afd1c /test/regress/regress0/bv | |
| parent | c05da2e3418f71ea7d9d8d59c76dc6773ead608b (diff) | |
Fix for bug 734
Diffstat (limited to 'test/regress/regress0/bv')
| -rw-r--r-- | test/regress/regress0/bv/Makefile.am | 1 | ||||
| -rw-r--r-- | test/regress/regress0/bv/bug734.smt2 | 9 |
2 files changed, 10 insertions, 0 deletions
diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am index 2caaea799..bb5c1e587 100644 --- a/test/regress/regress0/bv/Makefile.am +++ b/test/regress/regress0/bv/Makefile.am @@ -113,6 +113,7 @@ BUG_TESTS = \ bug260a.smt \ bug260b.smt \ bug440.smt \ + bug734.smt2 \ bug_extract_mult_leading_bit.smt2 TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS) diff --git a/test/regress/regress0/bv/bug734.smt2 b/test/regress/regress0/bv/bug734.smt2 new file mode 100644 index 000000000..1747c6cc4 --- /dev/null +++ b/test/regress/regress0/bv/bug734.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: sat +(set-logic QF_BV) +(declare-fun x0 () (_ BitVec 3)) +(assert (not (= #b001 x0))) +(assert (bvult #b000 x0)) +(check-sat) +(check-sat) |