smt parser for bit-vectors

1 files changed, 49 insertions, 0 deletions

diff --git a/test/regress/regress0/bv/test00.smt b/test/regress/regress0/bv/test00.smt
new file mode 100644
index 000000000..20fe6811f
--- /dev/null
+++ b/test/regress/regress0/bv/test00.smt
@@ -0,0 +1,49 @@
+(benchmark umulov1bw016.smt
+:source {
+We verify the correctness of an unsigned multiplication
+overflow detection unit, which is described in
+"Combined Unsigned and Two's Complement Saturating Multipliers"
+by M. Schulte et al.
+
+Bit-width: 4
+
+Contributed by Robert Brummayer (robert.brummayer@gmail.com).
+}
+:status unsat
+:category { industrial }
+:logic QF_BV
+:difficulty { 0 }
+:extrafuns ((v1 BitVec[4]))
+:extrafuns ((v2 BitVec[4]))
+:formula
+(let (?e3 bv0[4])
+(let (?e4 (concat ?e3 v1))
+(let (?e5 (concat ?e3 v2))
+(let (?e6 (bvmul ?e4 ?e5))
+(let (?e7 (extract[7:4] ?e6))
+(let (?e8 (ite (= ?e7 ?e3) bv1[1] bv0[1]))
+
+(let (?e32 (extract[3:3] v2))
+(let (?e34 (extract[2:2] v2))
+(let (?e35 (bvand (bvnot ?e32) (bvnot ?e34)))
+(let (?e36 (extract[1:1] v2))
+(let (?e37 (bvand ?e35 (bvnot ?e36)))
+(let (?e38 (extract[1:1] v1))
+
+(let (?e39 (bvand ?e38 ?e32))
+(let (?e40 (extract[2:2] v1))
+(let (?e41 (bvand ?e40 (bvnot ?e35)))
+(let (?e42 (bvand (bvnot ?e39) (bvnot ?e41)))
+(let (?e43 (extract[3:3] v1))
+(let (?e44 (bvand ?e43 (bvnot ?e37)))
+(let (?e45 (bvand ?e42 (bvnot ?e44)))
+
+(let (?e82 bv0[1])
+(let (?e83 (concat ?e82 v1))
+(let (?e84 (concat ?e82 v2))
+(let (?e85 (bvmul ?e83 ?e84))
+(let (?e86 (extract[4:4] ?e85))
+(let (?e87 (bvand ?e45 (bvnot ?e86)))
+(let (?e88 (ite (= (bvnot ?e8) (bvnot ?e87)) bv1[1] bv0[1]))
+(not (= (bvnot ?e88) bv0[1]))
+)))))))))))))))))))))))))))