diff options
Diffstat (limited to 'src/lfsc/tests/bv_mult10.smt2')
| -rw-r--r-- | src/lfsc/tests/bv_mult10.smt2 | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/src/lfsc/tests/bv_mult10.smt2 b/src/lfsc/tests/bv_mult10.smt2 new file mode 100644 index 0000000..38b8dec --- /dev/null +++ b/src/lfsc/tests/bv_mult10.smt2 @@ -0,0 +1,16 @@ +(set-logic QF_BV) +(declare-fun a () (_ BitVec 10)) +(declare-fun b () (_ BitVec 10)) +(declare-fun c () (_ BitVec 10)) +(declare-fun d () (_ BitVec 10)) + +(assert (= #b0000000010 a)) +(assert (= #b0000000110 b)) +(assert (= #b0000001000 c)) +(assert (= #b0000001100 d)) + +(assert + (not (= (bvmul a b) d))) + +(check-sat) +(exit) |