diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-01-03 09:35:27 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-01-03 09:35:27 -0600 |
commit | 1a11e8a71812d1abbf3fb13230c233d741c81fd1 (patch) | |
tree | 81be35f5bd356ca6b234ef49e62e966e062eec24 /test/regress | |
parent | e75a0d05db7133a90ec1fc4b9178c324e910b799 (diff) |
Global negate (#1466)
Diffstat (limited to 'test/regress')
-rw-r--r-- | test/regress/regress0/quantifiers/Makefile.am | 3 | ||||
-rw-r--r-- | test/regress/regress0/quantifiers/lra-triv-gn.smt2 | 7 |
2 files changed, 9 insertions, 1 deletions
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index a8c25ae5a..133c2018d 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -135,7 +135,8 @@ TESTS = \ clock-10.smt2 \ javafe.tc.FlowInsensitiveChecks.682.smt2 \ javafe.tc.CheckCompilationUnit.001.smt2 \ - model_6_1_bv.smt2 + model_6_1_bv.smt2 \ + lra-triv-gn.smt2 # regression can be solved with --finite-model-find --fmf-inst-engine diff --git a/test/regress/regress0/quantifiers/lra-triv-gn.smt2 b/test/regress/regress0/quantifiers/lra-triv-gn.smt2 new file mode 100644 index 000000000..ccd31c463 --- /dev/null +++ b/test/regress/regress0/quantifiers/lra-triv-gn.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --global-negate --no-check-unsat-cores +; EXPECT: unsat +(set-logic LRA) +(set-info :status unsat) +(assert (not (exists ((?X Real)) (>= (/ (- 13) 4) ?X)))) +(check-sat) +(exit)
\ No newline at end of file |