diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-04-29 22:05:53 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-04-29 22:05:53 -0500 |
| commit | b260533f7b2c5fc217fa0f5036ab121249829bd4 (patch) | |
| tree | c733ce57b0ab14b3e121842629a382964a51f536 /test/regress/regress1/nl | |
| parent | c3011ddae1d56eef2c7602b477c8935670a8aa75 (diff) | |
Make factoring inference more aggressive (#1825)
Diffstat (limited to 'test/regress/regress1/nl')
| -rw-r--r-- | test/regress/regress1/nl/factor_agg_s.smt2 | 10 | ||||
| -rw-r--r-- | test/regress/regress1/nl/nl_uf_lalt.smt2 | 9 |
2 files changed, 19 insertions, 0 deletions
diff --git a/test/regress/regress1/nl/factor_agg_s.smt2 b/test/regress/regress1/nl/factor_agg_s.smt2 new file mode 100644 index 000000000..4497f4c29 --- /dev/null +++ b/test/regress/regress1/nl/factor_agg_s.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --decision=justification --no-check-models +; EXPECT: sat +(set-logic QF_NRA) +(set-info :status sat) +(declare-fun skoX () Real) +(declare-fun skoY () Real) +(declare-fun skoZ () Real) +(assert (let ((?v_2 (<= 0 skoY)) (?v_0 (* skoX (- 1)))) (let ((?v_3 (* skoZ (+ 1 (* skoY ?v_0)))) (?v_4 (<= (* skoZ (+ (- 1) (* skoY skoX))) (+ skoX skoY)))) (let ((?v_1 (not ?v_4)) (?v_5 (* skoX ?v_0))) (let ((?v_6 (* skoY (* skoX (+ (- 3) ?v_5))))) (and (<= ?v_3 (+ ?v_0 (* skoY (- 1)))) (and ?v_1 (and (or ?v_1 ?v_2) (and (or ?v_2 (<= ?v_3 (+ (+ 1 ?v_0) (* skoY (+ (- 1) ?v_0))))) (and (or (not ?v_2) (or ?v_4 (<= (* skoZ (+ (+ 3 (* skoX skoX)) ?v_6)) (+ (* skoX ?v_5) (* skoY (+ (* skoX (* skoX (- 3))) ?v_6)))))) (and (not (<= skoZ 0)) (and (not (<= skoX (- 1))) (and (not (<= 1 skoY)) (not (<= skoY skoX))))))))))))))) +(check-sat) +(exit) diff --git a/test/regress/regress1/nl/nl_uf_lalt.smt2 b/test/regress/regress1/nl/nl_uf_lalt.smt2 new file mode 100644 index 000000000..5e8987d5b --- /dev/null +++ b/test/regress/regress1/nl/nl_uf_lalt.smt2 @@ -0,0 +1,9 @@ +(set-logic QF_UFNIA) +(set-info :status unsat) +(declare-fun c (Int) Int) +(declare-fun a (Int) Int) +(declare-fun b (Int) Int) +(assert (> (a 0) 0)) +(assert (= (c 0) (* (a 0) (b 0)))) +(assert (not (= (b 0) (div (c 0) (a 0))))) +(check-sat) |