diff options
Diffstat (limited to 'test/regress/regress0/bv/bv-options2.smt2')
| -rw-r--r-- | test/regress/regress0/bv/bv-options2.smt2 | 24 |
1 files changed, 0 insertions, 24 deletions
diff --git a/test/regress/regress0/bv/bv-options2.smt2 b/test/regress/regress0/bv/bv-options2.smt2 deleted file mode 100644 index d1ee44084..000000000 --- a/test/regress/regress0/bv/bv-options2.smt2 +++ /dev/null @@ -1,24 +0,0 @@ -; SCRUBBER: sed -e 's/(error \"Error.in.option.parsing.*$/Error in option parsing/' -; EXPECT: Error in option parsing -; COMMAND-LINE: --check-proofs --bv-eq-solver -; EXIT: 1 -(set-logic QF_BV) -(set-info :smt-lib-version 2.0) -(set-info :category "crafted") -(declare-fun v0 () (_ BitVec 16)) -(declare-fun v1 () (_ BitVec 16)) -(declare-fun v2 () (_ BitVec 16)) -(declare-fun v3 () (_ BitVec 16)) -(declare-fun v4 () (_ BitVec 16)) -(declare-fun v5 () (_ BitVec 16)) -(assert (and - (bvult v2 v4) - (bvult v3 v4) - (bvult v0 v1) - (bvult v1 v2) - (bvult v1 v3) - (bvult v4 v5) - (bvult v5 v1) - )) -(check-sat) -(exit) |