diff options
Diffstat (limited to 'test/regress/regress0')
| -rw-r--r-- | test/regress/regress0/fmf/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/fmf/krs-sat.smt2 | 16 | ||||
| -rw-r--r-- | test/regress/regress0/quantifiers/Makefile.am | 5 | ||||
| -rw-r--r-- | test/regress/regress0/quantifiers/ari056.smt2 | 4 |
4 files changed, 25 insertions, 3 deletions
diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am index 9d6df2796..bb85e62b3 100644 --- a/test/regress/regress0/fmf/Makefile.am +++ b/test/regress/regress0/fmf/Makefile.am @@ -40,7 +40,8 @@ TESTS = \ fib-core.smt2 \ fore19-exp2-core.smt2 \ with-ind-104-core.smt2 \ - syn002-si-real-int.smt2 + syn002-si-real-int.smt2 \ + krs-sat.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/fmf/krs-sat.smt2 b/test/regress/regress0/fmf/krs-sat.smt2 new file mode 100644 index 000000000..22d9e4474 --- /dev/null +++ b/test/regress/regress0/fmf/krs-sat.smt2 @@ -0,0 +1,16 @@ +; COMMAND-LINE: --finite-model-find +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(declare-sort $$unsorted 0) +(declare-fun cowlNothing ($$unsorted) Bool) +(declare-fun cowlThing ($$unsorted) Bool) +(declare-fun xsd_integer ($$unsorted) Bool) +(declare-fun xsd_string ($$unsorted) Bool) +(declare-fun is () $$unsorted) +(assert (and (forall ((X $$unsorted)) (cowlThing X) ) (forall ((X $$unsorted)) (not (cowlNothing X)) ))) +(assert (forall ((X $$unsorted)) (= (xsd_string X) (not (xsd_integer X))) )) +(assert (and (forall ((X $$unsorted)) (or (not (cowlThing X)) (= X is)) ) (cowlThing is))) +(assert (cowlThing is)) +(assert (and (forall ((X $$unsorted)) (cowlThing X) ) (forall ((X $$unsorted)) (not (cowlNothing X)) ) (forall ((X $$unsorted)) (or (not (cowlThing X)) (= X is)) ))) +(check-sat) diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index 89dcc0a26..e6b0a59fc 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -59,8 +59,9 @@ TESTS = \ floor.smt2 \ array-unsat-simp3.smt2 \ mix-simp.smt2 \ - mix-coeff.smt2 \ - mix-match.smt2 + mix-coeff.smt2 \ + mix-match.smt2 \ + ari056.smt2 # regression can be solved with --finite-model-find --fmf-inst-engine diff --git a/test/regress/regress0/quantifiers/ari056.smt2 b/test/regress/regress0/quantifiers/ari056.smt2 new file mode 100644 index 000000000..ed4d2bf4a --- /dev/null +++ b/test/regress/regress0/quantifiers/ari056.smt2 @@ -0,0 +1,4 @@ +(set-logic UFNIRA) +(set-info :status unsat) +(assert (forall ((X Int)) (= X 12) )) +(check-sat) |