diff options
Diffstat (limited to 'src/lfsc/tests/bv_add.smt2')
| -rw-r--r-- | src/lfsc/tests/bv_add.smt2 | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/src/lfsc/tests/bv_add.smt2 b/src/lfsc/tests/bv_add.smt2 new file mode 100644 index 0000000..dd7586e --- /dev/null +++ b/src/lfsc/tests/bv_add.smt2 @@ -0,0 +1,16 @@ +(set-logic QF_BV) +(declare-fun a () (_ BitVec 4)) +(declare-fun b () (_ BitVec 4)) +(declare-fun c () (_ BitVec 4)) +(declare-fun d () (_ BitVec 4)) + +(assert (= #b0010 a)) +(assert (= #b0110 b)) +(assert (= #b1000 c)) +(assert (= #b1100 d)) + +(assert + (not (= (bvadd a b) c))) + +(check-sat) +(exit) |