diff options
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/Makefile.tests | 2 | ||||
| -rw-r--r-- | test/regress/regress1/nl/factor_agg_s.smt2 | 10 | ||||
| -rw-r--r-- | test/regress/regress1/nl/nl_uf_lalt.smt2 | 9 |
3 files changed, 21 insertions, 0 deletions
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index 5b12c005c..1ec6323b2 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1117,6 +1117,7 @@ REG1_TESTS = \ regress1/nl/exp-4.5-lt.smt2 \ regress1/nl/exp1-lb.smt2 \ regress1/nl/exp_monotone.smt2 \ + regress1/nl/factor_agg_s.smt2 \ regress1/nl/metitarski-1025.smt2 \ regress1/nl/metitarski-3-4.smt2 \ regress1/nl/metitarski_3_4_2e.smt2 \ @@ -1124,6 +1125,7 @@ REG1_TESTS = \ regress1/nl/nl-eq-infer.smt2 \ regress1/nl/nl-help-unsat-quant.smt2 \ regress1/nl/nl-unk-quant.smt2 \ + regress1/nl/nl_uf_lalt.smt2 \ regress1/nl/ones.smt2 \ regress1/nl/poly-1025.smt2 \ regress1/nl/quant-nl.smt2 \ 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) |