Fixes 2 issues with assignments. The first is constructing an initial assignment for slack variables once solving has begun. (They cannot just be 0.) The second has to do with how assignments are backttacked. Assignments are now tracked all of the time, and are frozen once they are known to be consistent, i.e. after a successful updateInconsistentVars(). Also added a fuzz test that shows both of these problems to the regressions.

1 files changed, 46 insertions, 0 deletions

diff --git a/test/regress/regress0/fuzz_3.smt b/test/regress/regress0/fuzz_3.smt
new file mode 100644
index 000000000..e1c53d2c3
--- /dev/null
+++ b/test/regress/regress0/fuzz_3.smt
@@ -0,0 +1,46 @@
+(benchmark fuzzsmt
+:logic QF_LRA
+:extrafuns ((v0 Real))
+:extrafuns ((v2 Real))
+:extrafuns ((v1 Real))
+:status sat
+:formula
+(let (?n1 2)
+(let (?n2 (* ?n1 ?n1))
+(let (?n3 (~ v0))
+(let (?n4 (* ?n1 ?n3))
+(let (?n5 (- ?n1 ?n1))
+(let (?n6 (- ?n5 v0))
+(let (?n7 (- ?n4 ?n6))
+(flet ($n8 (= ?n2 ?n7))
+(flet ($n9 false)
+(let (?n10 (ite $n9 ?n1 v1))
+(let (?n11 (+ ?n1 v2))
+(flet ($n12 (<= ?n10 ?n11))
+(let (?n13 (ite $n9 v0 ?n2))
+(let (?n14 (~ ?n1))
+(let (?n15 (ite $n9 ?n14 ?n1))
+(flet ($n16 (< ?n13 ?n15))
+(flet ($n17 (= ?n1 ?n7))
+(let (?n18 (+ ?n1 ?n1))
+(flet ($n19 (= v2 ?n18))
+(let (?n20 (ite $n19 v2 ?n1))
+(let (?n21 (ite $n17 ?n18 ?n20))
+(flet ($n22 (>= ?n21 ?n2))
+(let (?n23 (ite $n9 ?n21 ?n2))
+(flet ($n24 (<= ?n23 ?n1))
+(flet ($n25 (> ?n7 ?n2))
+(flet ($n26 (iff $n24 $n25))
+(let (?n27 (~ ?n7))
+(flet ($n28 (<= ?n27 ?n1))
+(let (?n29 (ite $n28 ?n1 ?n1))
+(flet ($n30 (< ?n1 ?n29))
+(flet ($n31 (implies $n26 $n30))
+(flet ($n32 (implies $n9 $n9))
+(flet ($n33 (if_then_else $n22 $n31 $n32))
+(flet ($n34 (and $n9 $n33))
+(flet ($n35 (if_then_else $n16 $n34 $n9))
+(flet ($n36 (iff $n12 $n35))
+(flet ($n37 (and $n8 $n36))
+$n37
+))))))))))))))))))))))))))))))))))))))