diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-10-18 19:37:11 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-10-18 19:37:11 -0500 |
| commit | 547bd91e189b28da9950e12037d1e88079157479 (patch) | |
| tree | 7f225e6df081071028c9e6102c902a6224179edf /test/regress/regress1/nl | |
| parent | 10707e3ec6f2cab793919f2d1a159e13cdd032a9 (diff) | |
Non-implied mode for model cores (#2653)
Diffstat (limited to 'test/regress/regress1/nl')
| -rw-r--r-- | test/regress/regress1/nl/pinto-model-core-ni.smt2 | 22 |
1 files changed, 22 insertions, 0 deletions
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) |