Changes to the combination mechanism, lots of details. Not done yet, there are still the AUFBV wrong results, but it seems better.

http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=4382&reference_id=4359&p=5

3 files changed, 128 insertions, 1 deletions

diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am
index 5048ca680..07619b965 100644
--- a/test/regress/regress0/bv/Makefile.am
+++ b/test/regress/regress0/bv/Makefile.am
@@ -28,7 +28,8 @@ SMT_TESTS = \
 	fuzz11.smt \
 	fuzz12.smt \
 	fuzz13.smt \
-	fuzz14.smt
+	fuzz14.smt \
+	calc2_sec2_shifter_mult_bmc15.atlas.delta01.smt
 
 # Regression tests for SMT2 inputs
 SMT2_TESTS =
diff --git a/test/regress/regress0/bv/bug345.smt b/test/regress/regress0/bv/bug345.smt
new file mode 100644
index 000000000..b836cba2c
--- /dev/null
+++ b/test/regress/regress0/bv/bug345.smt
@@ -0,0 +1,46 @@
+(benchmark B_
+:logic QF_AUFBV
+:extrafuns ((mem_35_197 Array[32:8]))
+:status unknown
+:formula
+(let (?n1 bv1[1])
+(let (?n2 bv0[31])
+(let (?n3 bv0[32])
+(let (?n4 bv0[24])
+(let (?n5 (select mem_35_197 ?n3))
+(let (?n6 (concat ?n4 ?n5))
+(flet ($n7 (= ?n3 ?n6))
+(let (?n8 bv0[1])
+(let (?n9 (ite $n7 ?n1 ?n8))
+(let (?n10 (concat ?n2 ?n9))
+(let (?n11 (extract[0:0] ?n10))
+(let (?n12 bv0[8])
+(let (?n13 bv1[32])
+(let (?n14 (select mem_35_197 ?n13))
+(let (?n15 (concat ?n4 ?n14))
+(let (?n16 (extract[7:0] ?n15))
+(flet ($n17 (= ?n12 ?n16))
+(let (?n18 bv1[8])
+(flet ($n19 (= ?n16 ?n18))
+(let (?n20 bv3[8])
+(flet ($n21 (= ?n16 ?n20))
+(let (?n22 (ite $n21 ?n13 ?n3))
+(let (?n23 (ite $n19 ?n3 ?n22))
+(let (?n24 (ite $n17 ?n13 ?n23))
+(let (?n25 (extract[7:0] ?n24))
+(let (?n26 (store mem_35_197 ?n3 ?n25))
+(let (?n27 (concat ?n4 ?n16))
+(let (?n28 (extract[7:0] ?n27))
+(let (?n29 (concat ?n4 ?n28))
+(let (?n30 (extract[7:0] ?n29))
+(let (?n31 (concat ?n4 ?n30))
+(let (?n32 (bvadd ?n6 ?n31))
+(let (?n33 (store ?n26 ?n32 ?n12))
+(let (?n34 (select ?n33 ?n3))
+(let (?n35 (concat ?n4 ?n34))
+(flet ($n36 (= ?n3 ?n35))
+(let (?n37 (ite $n36 ?n1 ?n8))
+(let (?n38 (bvor ?n11 ?n37))
+(flet ($n39 (= ?n1 ?n38))
+$n39
+))))))))))))))))))))))))))))))))))))))))
diff --git a/test/regress/regress0/bv/calc2_sec2_shifter_mult_bmc15.atlas.delta01.smt b/test/regress/regress0/bv/calc2_sec2_shifter_mult_bmc15.atlas.delta01.smt
new file mode 100644
index 000000000..467f10c39
--- /dev/null
+++ b/test/regress/regress0/bv/calc2_sec2_shifter_mult_bmc15.atlas.delta01.smt
@@ -0,0 +1,80 @@
+(benchmark B_
+:logic QF_BV
+:extrapreds ((UCL_p16))
+:extrapreds ((UCL_p34))
+:status sat
+:formula
+(let (?n1 bv1[1])
+(let (?n2 bv0[2])
+(let (?n3 bv1[5])
+(let (?n4 bv0[5])
+(let (?n5 bv0[4])
+(let (?n6 bv1[4])
+(let (?n7 (ite UCL_p16 ?n6 ?n5))
+(flet ($n8 (= ?n5 ?n7))
+(let (?n9 bv1[2])
+(let (?n10 (ite $n8 ?n9 ?n2))
+(flet ($n11 (= ?n2 ?n10))
+(flet ($n12 (= ?n9 ?n10))
+(flet ($n13 (or $n11 $n12))
+(let (?n14 (ite $n13 ?n3 ?n4))
+(flet ($n15 (= ?n4 ?n14))
+(let (?n16 (ite $n15 ?n3 ?n4))
+(flet ($n17 (= ?n4 ?n16))
+(let (?n18 (ite UCL_p34 ?n2 ?n9))
+(flet ($n19 (= ?n9 ?n18))
+(let (?n20 (ite $n19 ?n6 ?n5))
+(flet ($n21 (= ?n5 ?n20))
+(let (?n22 (ite $n21 ?n3 ?n4))
+(let (?n23 (bvadd ?n22 ?n16))
+(let (?n24 (bvadd ?n3 ?n23))
+(let (?n25 (ite $n17 ?n24 ?n23))
+(flet ($n26 (= ?n3 ?n25))
+(let (?n27 bv1[6])
+(let (?n28 (concat ?n27 ?n9))
+(let (?n29 bv0[32])
+(let (?n30 (concat ?n28 ?n29))
+(let (?n31 (concat ?n30 ?n29))
+(let (?n32 bv0[72])
+(let (?n33 (ite $n26 ?n31 ?n32))
+(let (?n34 (extract[67:64] ?n33))
+(let (?n35 (extract[3:2] ?n34))
+(flet ($n36 (= ?n2 ?n35))
+(let (?n37 (ite $n36 ?n9 ?n2))
+(flet ($n38 (= ?n2 ?n37))
+(let (?n39 bv0[3])
+(let (?n40 bv1[3])
+(let (?n41 (ite $n38 ?n39 ?n40))
+(let (?n42 (extract[0:0] ?n41))
+(flet ($n43 (= ?n1 ?n42))
+(let (?n44 (ite $n43 ?n9 ?n2))
+(let (?n45 (ite $n12 ?n3 ?n4))
+(flet ($n46 (= ?n4 ?n45))
+(let (?n47 (ite $n8 ?n3 ?n4))
+(flet ($n48 (= ?n4 ?n47))
+(let (?n49 (ite $n48 ?n14 ?n4))
+(flet ($n50 (= ?n4 ?n49))
+(let (?n51 (bvsub ?n4 ?n3))
+(let (?n52 (ite $n50 ?n4 ?n51))
+(flet ($n53 (= ?n4 ?n52))
+(let (?n54 (ite $n53 ?n3 ?n52))
+(let (?n55 (ite $n46 ?n4 ?n54))
+(flet ($n56 (= ?n3 ?n55))
+(let (?n57 (concat ?n6 ?n9))
+(let (?n58 (concat ?n57 ?n2))
+(let (?n59 (concat ?n58 ?n29))
+(let (?n60 (concat ?n59 ?n29))
+(let (?n61 (bvadd ?n45 ?n52))
+(flet ($n62 (= ?n3 ?n61))
+(let (?n63 (ite $n62 ?n32 ?n31))
+(let (?n64 (ite $n56 ?n60 ?n63))
+(let (?n65 (extract[67:64] ?n64))
+(let (?n66 (extract[3:2] ?n65))
+(flet ($n67 (= ?n2 ?n66))
+(let (?n68 (extract[71:68] ?n64))
+(flet ($n69 (= ?n5 ?n68))
+(let (?n70 (ite $n69 ?n2 ?n9))
+(let (?n71 (ite $n67 ?n70 ?n2))
+(flet ($n72 (= ?n44 ?n71))
+$n72
+)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))