diff --git a/tests/regress/wd/issue220.smt2 b/tests/regress/wd/issue220.smt2 new file mode 100644 index 000000000..78f8c2a60 --- /dev/null +++ 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 new file mode 100644 index 000000000..6b8a2c3d2 --- /dev/null +++ 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 new file mode 100644 index 000000000..ffbd89592 --- /dev/null +++ b/tests/regress/wd/issue220.smt2.options @@ -0,0 +1 @@ +--incremental