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

1 files changed, 36 insertions, 0 deletions

diff --git a/test/regress/regress0/aufbv/wchains010ue.delta01.smt b/test/regress/regress0/aufbv/wchains010ue.delta01.smt
new file mode 100644
index 000000000..28a892e8d
--- /dev/null
+++ b/test/regress/regress0/aufbv/wchains010ue.delta01.smt
@@ -0,0 +1,36 @@
+(benchmark wchains010ue.smt
+:logic QF_AUFBV
+:extrafuns ((v6 BitVec[32]))
+:extrafuns ((a1 Array[32:8]))
+:extrafuns ((v15 BitVec[32]))
+:status sat
+:formula
+(let (?n1 bv0[1])
+(let (?n2 (extract[1:0] v6))
+(let (?n3 bv0[2])
+(flet ($n4 (= ?n2 ?n3))
+(let (?n5 bv1[1])
+(let (?n6 (ite $n4 ?n5 ?n1))
+(let (?n7 bv0[8])
+(let (?n8 (store a1 v15 ?n7))
+(let (?n9 bv1[32])
+(let (?n10 (bvadd ?n9 v15))
+(let (?n11 (store ?n8 ?n10 ?n7))
+(let (?n12 bv3[32])
+(let (?n13 (bvadd ?n12 v15))
+(let (?n14 (store ?n11 ?n13 ?n7))
+(let (?n15 (extract[7:0] v6))
+(let (?n16 (store a1 v6 ?n15))
+(let (?n17 (bvadd ?n9 v6))
+(let (?n18 bv1[8])
+(let (?n19 (store ?n16 ?n17 ?n18))
+(let (?n20 (bvadd ?n12 v6))
+(let (?n21 (store ?n19 ?n20 ?n18))
+(flet ($n22 (= ?n14 ?n21))
+(let (?n23 (ite $n22 ?n5 ?n1))
+(let (?n24 (bvnot ?n23))
+(let (?n25 (bvand ?n6 ?n24))
+(flet ($n26 (= ?n1 ?n25))
+(flet ($n27 (not $n26))
+$n27
+))))))))))))))))))))))))))))