diff options
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/model-core.smt2 | 3 | ||||
| -rw-r--r-- | test/regress/regress1/nl/pinto-model-core-ni.smt2 | 22 |
3 files changed, 25 insertions, 1 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index a41108a71..cd98a8917 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1183,6 +1183,7 @@ set(regress_1_tests regress1/nl/nl-unk-quant.smt2 regress1/nl/nl_uf_lalt.smt2 regress1/nl/ones.smt2 + regress1/nl/pinto-model-core-ni.smt2 regress1/nl/poly-1025.smt2 regress1/nl/quant-nl.smt2 regress1/nl/red-exp.smt2 diff --git a/test/regress/regress0/model-core.smt2 b/test/regress/regress0/model-core.smt2 index 6729cb5e0..fca80a960 100644 --- a/test/regress/regress0/model-core.smt2 +++ b/test/regress/regress0/model-core.smt2 @@ -1,4 +1,5 @@ -; COMMAND-LINE: --produce-model-cores +; COMMAND-LINE: --produce-models --model-cores=simple +; COMMAND-LINE: --produce-models --model-core=non-implied ; EXPECT: sat (set-logic QF_UFLIA) (declare-fun x () Int) diff --git a/test/regress/regress1/nl/pinto-model-core-ni.smt2 b/test/regress/regress1/nl/pinto-model-core-ni.smt2 new file mode 100644 index 000000000..1e09f8439 --- /dev/null +++ b/test/regress/regress1/nl/pinto-model-core-ni.smt2 @@ -0,0 +1,22 @@ +; COMMAND-LINE: --nl-ext-tplanes --produce-models --model-core=non-implied +; EXPECT: sat +(set-logic ALL) +(declare-fun i1 () Real) +(declare-fun i2 () Real) +(declare-fun n () Int) +(declare-fun x () Int) +(declare-fun y () Int) +(declare-fun i11 () Real) +(declare-fun i21 () Real) + +(assert (>= n 1)) +(assert (and (<= 1 x)(<= x n))) +(assert (and (<= 1 y)(<= y n))) +(assert (or (= (/ (* (- 1) x) n) i1)(= i1 (/ x n)))) +(assert (or (= (/ (* (- 1) y) n) i2)(= i2 (/ y n)))) + +(assert (and (= i1 i11) (= i2 i21) )) + +(assert (not (and (or (= (- 1) i11 )(= i11 1)) (or (= (- 1) i21)(= i21 1)) ))) + +(check-sat) |