diff options
Diffstat (limited to 'test/regress/regress0/cvc3.userdoc.05.cvc.smt2')
| -rw-r--r-- | test/regress/regress0/cvc3.userdoc.05.cvc.smt2 | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/test/regress/regress0/cvc3.userdoc.05.cvc.smt2 b/test/regress/regress0/cvc3.userdoc.05.cvc.smt2 new file mode 100644 index 000000000..d72acbc57 --- /dev/null +++ b/test/regress/regress0/cvc3.userdoc.05.cvc.smt2 @@ -0,0 +1,8 @@ +; EXPECT: unsat +(set-logic ALL) +(set-option :incremental false) +(declare-fun x () (_ BitVec 4)) +(declare-fun y () (_ BitVec 4)) +(assert (= x #b0101)) +(assert (= y #b0101)) +(check-sat-assuming ( (not (let ((_let_1 (bvneg x))) (let ((_let_2 ((_ zero_extend 4) x))) (let ((_let_3 ((_ zero_extend 4) y))) (and (and (and (= (bvmul _let_2 _let_3) (bvmul _let_3 _let_2)) (not (bvult x y))) (bvule (bvsub _let_2 _let_3) (bvadd _let_2 ((_ zero_extend 4) _let_1)))) (= x (bvsub _let_1 (bvadd x #b0001)))))))) )) |