1 files changed, 22 insertions, 0 deletions
diff --git a/test/regress/regress1/quantifiers/smtcomp-qbv-053118.smt2 b/test/regress/regress1/quantifiers/smtcomp-qbv-053118.smt2
new file mode 100644
index 000000000..6cbe4db5c
--- /dev/null
+++ b/test/regress/regress1/quantifiers/smtcomp-qbv-053118.smt2
@@ -0,0 +1,22 @@
+(set-info :smt-lib-version 2.6)
+(set-logic BV)
+(set-info :status sat)
+(declare-fun x () (_ BitVec 32))
+(assert 
+(forall ((u (_ BitVec 32)) (w (_ BitVec 32)) (z (_ BitVec 32)) (m (_ BitVec 32)) (n (_ BitVec 32))) (or 
+  (not (= 
+    (bvadd (bvmul (_ bv2 32) w) (bvmul (_ bv2 32) n)) 
+    (bvadd (bvneg (bvadd (bvmul (_ bv2 32) u) (bvmul (_ bv2 32) z) (bvmul (_ bv2 32) m) x)) (_ bv1 32))
+  )) 
+))
+)
+(assert (not 
+(and 
+  (forall ((m (_ BitVec 32)) (n (_ BitVec 32))) 
+    (not (= 
+      (bvadd (bvneg (bvadd m x)) (_ bv1 32)) 
+      (bvmul (_ bv2 32) n)
+    ))
+))))
+(check-sat)
+(exit)