diff options
Diffstat (limited to 'test')
| -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 |