Regression test

SRI-CSL · Jun 18, 2020 · 305a800 · 305a800
1 parent d554286
commit 305a800
Show file tree

Hide file tree

Showing 3 changed files with 19 additions and 0 deletions.
diff --git a/tests/regress/wd/issue220.smt2 b/tests/regress/wd/issue220.smt2
@@ -0,0 +1,17 @@
+(set-logic QF_BV)
+(declare-const x (_ BitVec 5))
+(assert
+ (=
+  (bvadd
+   (bvmul (concat (_ bv64 5) x) (concat (_ bv64 5) x))
+   (concat (_ bv64 5) x)
+   (bvmul (concat (_ bv64 5) x) (concat (_ bv64 5) x)))
+
+  (bvadd
+   (concat (_ bv64 5) x)
+   (bvmul (concat (_ bv64 5) x) (concat (_ bv64 5) x)))
+
+  (concat (_ bv64 5) x)))
+
+(check-sat)
+
diff --git a/tests/regress/wd/issue220.smt2.gold b/tests/regress/wd/issue220.smt2.gold
@@ -0,0 +1 @@
+sat
diff --git a/tests/regress/wd/issue220.smt2.options b/tests/regress/wd/issue220.smt2.options
@@ -0,0 +1 @@
+--incremental