diff options
| author | Tim King <taking@cs.nyu.edu> | 2012-11-12 22:54:35 +0000 |
|---|---|---|
| committer | Tim King <taking@cs.nyu.edu> | 2012-11-12 22:54:35 +0000 |
| commit | 8c325a4bf6888e33fb8fdc1e071a8aab4aa20b6f (patch) | |
| tree | 0132d93da953d48f57b0b0ed125c6de19c2c6e29 /test/regress/regress0/arith | |
| parent | 069feb82d76d10bbeebcf93a00d85b7caedb2d36 (diff) | |
Delta is now generated in arithmetic to keep consistent the total order of DeltaRational values for lowerbounds, upperbounds, assignments and disequalities. Throws LogicException when a non-linear term is asserted and the the LogicInfo isLinear() disagrees.
Diffstat (limited to 'test/regress/regress0/arith')
| -rw-r--r-- | test/regress/regress0/arith/Makefile.am | 4 | ||||
| -rw-r--r-- | test/regress/regress0/arith/bug443.delta01.smt | 37 | ||||
| -rw-r--r-- | test/regress/regress0/arith/mult.02.smt2 | 11 |
3 files changed, 51 insertions, 1 deletions
diff --git a/test/regress/regress0/arith/Makefile.am b/test/regress/regress0/arith/Makefile.am index a30c99462..12aa0eecd 100644 --- a/test/regress/regress0/arith/Makefile.am +++ b/test/regress/regress0/arith/Makefile.am @@ -36,7 +36,9 @@ TESTS = \ div.06.smt2 \ div.07.smt2 \ div.08.smt2 \ - mult.01.smt2 + mult.01.smt2 \ + mult.02.smt2 \ + bug443.delta01.smt # problem__003.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/arith/bug443.delta01.smt b/test/regress/regress0/arith/bug443.delta01.smt new file mode 100644 index 000000000..0b8a0d971 --- /dev/null +++ b/test/regress/regress0/arith/bug443.delta01.smt @@ -0,0 +1,37 @@ +(benchmark fuzzsmt +:logic QF_UFLRA +:extrafuns ((v1 Real)) +:extrafuns ((v2 Real)) +:extrafuns ((v0 Real)) +:extrapreds ((p1 Real)) +:status sat +:formula +(let (?n1 0) +(flet ($n2 (p1 ?n1)) +(let (?n3 1) +(flet ($n4 (= ?n3 v2)) +(let (?n5 5) +(let (?n6 (~ ?n5)) +(let (?n7 (* v2 ?n6)) +(let (?n8 (+ ?n7 v1)) +(flet ($n9 (= ?n5 ?n8)) +(let (?n10 (ite $n9 ?n3 v1)) +(flet ($n11 (= ?n7 ?n10)) +(flet ($n12 (p1 v0)) +(let (?n13 (ite $n12 ?n1 v1)) +(flet ($n14 (p1 ?n13)) +(let (?n15 (~ ?n7)) +(let (?n16 (- ?n3 ?n15)) +(flet ($n17 (>= ?n16 ?n8)) +(flet ($n18 (> ?n16 ?n1)) +(flet ($n19 (= ?n8 v0)) +(let (?n20 (ite $n19 ?n8 ?n16)) +(let (?n21 (ite $n18 ?n20 ?n7)) +(let (?n22 (ite $n17 ?n21 v2)) +(flet ($n23 (> ?n22 v1)) +(flet ($n24 (implies $n14 $n23)) +(flet ($n25 (and $n11 $n24)) +(flet ($n26 (implies $n4 $n25)) +(flet ($n27 (xor $n2 $n26)) +$n27 +)))))))))))))))))))))))))))) diff --git a/test/regress/regress0/arith/mult.02.smt2 b/test/regress/regress0/arith/mult.02.smt2 new file mode 100644 index 000000000..d690e38e8 --- /dev/null +++ b/test/regress/regress0/arith/mult.02.smt2 @@ -0,0 +1,11 @@ +; EXPECT: (error "Non-linear term was asserted to arithmetic in a linear logic.") +; EXIT: 1 +(set-logic QF_LRA) +(set-info :status unknown) +(declare-fun n () Real) + +; This example is test that LRA rejects multiplication terms + +(assert (= (* n n) 1)) + +(check-sat) |