Add regressions from #3687. (#5553)

The error from #3687 has been fixed in the meantime.
This PR adds the two examples from this issue as regressions.
Closes #3687

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index fda5c69eb9d3ad0d5734e99f02dbf4e79f399ad4..1826b31562368230b54e7eac975ed4dda45bec46 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -126,6 +126,7 @@ set(regress_0_tests
   regress0/aufbv/fuzz14.smtv1.smt2
   regress0/aufbv/fuzz15.smtv1.smt2
   regress0/aufbv/issue3737.smt2
+  regress0/aufbv/issue3687-check-models-small.smt2
   regress0/aufbv/rewrite_bug.smtv1.smt2
   regress0/aufbv/try3_sameret_functions_fse-bfs_tac.calc_next.il.fse-bfs.delta01.smtv1.smt2
   regress0/aufbv/try5_small_difret_functions_wp_su.set_char_quoting.il.wp.delta01.smtv1.smt2
@@ -2176,6 +2177,7 @@ set(regress_2_tests
   regress2/hole7.cvc
   regress2/hole8.cvc
   regress2/instance_1444.smtv1.smt2
+  regress2/issue3687-check-models.smt2
   regress2/issue4707-bv-to-bool-large.smt2
   regress2/javafe.ast.StandardPrettyPrint.319_no_forall.smt2
   regress2/javafe.ast.WhileStmt.447_no_forall.smt2

diff --git a/test/regress/regress0/aufbv/issue3687-check-models-small.smt2 b/test/regress/regress0/aufbv/issue3687-check-models-small.smt2
new file mode 100644 (file)
index 0000000..88cbd8a
--- /dev/null
+++ b/test/regress/regress0/aufbv/issue3687-check-models-small.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --check-models
+; EXPECT: sat
+(set-logic QF_AUFBV)
+(declare-fun a () (Array (_ BitVec 2) (_ BitVec 2)))
+(declare-fun b () (_ BitVec 2))
+(assert (distinct #b01 (select (store (store a #b01 (bvor #b01 (select a
+  #b00))) #b10 #b00) b)))
+(check-sat)
\ No newline at end of file

diff --git a/test/regress/regress2/issue3687-check-models.smt2 b/test/regress/regress2/issue3687-check-models.smt2
new file mode 100644 (file)
index 0000000..02f7754
--- /dev/null
+++ b/test/regress/regress2/issue3687-check-models.smt2
@@ -0,0 +1,51 @@
+; COMMAND-LINE: --check-models
+; EXPECT: sat
+(set-logic QF_ABV)
+(declare-fun c () (_ BitVec 32))
+(declare-fun a () (Array (_ BitVec 32) (_ BitVec 8)))
+(declare-fun b () (_ BitVec 32))
+(assert (let ((a!1 (bvxnor (concat #x000000 (select a (bvadd c #x00000001))) #x00000008))
+      (a!3 (bvsdiv (concat #x000000 (select a (bvadd c #x00000002))) #x00000010))
+      (a!4 (bvudiv (concat #x000000 (select a (bvashr c #x00000003)))
+                   #x00000018))
+      (a!5 (select a
+                   (bvxor (bvsub (bvnand c #x00000004) #x00000004) #x00000000)))
+      (a!6 (select a
+                   (bvsdiv (bvsub (bvnand c #x00000004) #x00000004) #x00000001)))
+      (a!7 (select a
+                   (bvadd (bvsub (bvnand c #x00000004) #x00000004) #x00000002)))
+      (a!9 (store a
+                  (bvashr (bvurem (bvnand c #x00000004) #x00000004) #x00000001)
+                  ((_ extract 7 0) (bvxnor b #x00000008))))
+      (a!11 (bvnand (bvurem (bvsub (bvnand c #x00000004) #x00000004) #x00000004)
+                    #x00000008)))
+(let ((a!2 (bvnor (concat #x000000 (select a (bvsmod c #x00000000))) a!1))
+      (a!8 (bvlshr (bvor (concat #x000000 a!5)
+                         (bvmul (concat #x000000 a!6) #x00000008))
+                   (bvand (concat #x000000 a!7) #x00000010)))
+      (a!10 (store a!9
+                   (bvshl (bvurem (bvnand c #x00000004) #x00000004) #x00000000)
+                   ((_ extract 7 0) b)))
+      (a!12 (bvsub (concat #x000000 (select a (bvashr a!11 #x00000001)))
+                   #x00000008))
+      (a!14 (bvxnor (concat #x000000 (select a (bvxnor a!11 #x00000002)))
+                    #x00000010))
+      (a!15 (bvxor (concat #x000000 (select a (bvsub a!11 #x00000003)))
+                   #x00000018)))
+(let ((a!13 (bvor (concat #x000000 (select a (bvmul a!11 #x00000000))) a!12)))
+(let ((a!16 ((_ extract 7 0)
+              (bvmul (bvurem (bvurem a!13 a!14) a!15) #x00000018)))
+      (a!17 ((_ extract 7 0) (bvor (bvurem (bvurem a!13 a!14) a!15) #x00000010)))
+      (a!18 ((_ extract 7 0)
+              (bvnor (bvurem (bvurem a!13 a!14) a!15) #x00000008))))
+(let ((a!19 (store (store (store (store a!10 #x08053e77 a!16) #x08053e76 a!17)
+                          #x08053e75
+                          a!18)
+                   #x08053e74
+                   ((_ extract 7 0) (bvurem (bvurem a!13 a!14) a!15)))))
+(let ((a!20 (select a!19
+                    (bvadd (bvsub (bvnand c #x00000004) #x00000004) #x00000003))))
+(let ((a!21 (distinct (bvsdiv (bvsmod a!2 a!3) a!4)
+                      (bvshl a!8 (bvshl (concat #x000000 a!20) #x00000018)))))
+  (= #b1 (bvashr (ite (or a!21) #b1 #b0) #b1))))))))))
+(check-sat)