diff options
author | Tim King <taking@cs.nyu.edu> | 2010-06-03 20:34:21 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2010-06-03 20:34:21 +0000 |
commit | 4cd2a432d621d18f7b811caab8935a617b4771c5 (patch) | |
tree | 77ddbe1e674df7f04a85f3ae5896f310ade13258 /test/regress/regress0 | |
parent | 9e43f4ea07dc7d20be5ce31e8569bbfda4069432 (diff) |
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.
Diffstat (limited to 'test/regress/regress0')
-rw-r--r-- | test/regress/regress0/Makefile.am | 3 | ||||
-rw-r--r-- | test/regress/regress0/fuzz_3.smt | 46 |
2 files changed, 48 insertions, 1 deletions
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 515d496f5..0b8a60495 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -55,7 +55,8 @@ TESTS = \ wiki.18.cvc \ wiki.19.cvc \ wiki.20.cvc \ - wiki.21.cvc + wiki.21.cvc \ + fuzz_3.smt if CVC4_BUILD_PROFILE_COMPETITION else 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 +)))))))))))))))))))))))))))))))))))))) |