diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2021-01-29 19:34:57 -0300 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-01-29 19:34:57 -0300 |
| commit | 9ae030595825ad57bdbf55d856627318913c2fcf (patch) | |
| tree | a6b0b6c8e444777a2fba3c3b6fcd4bbddcd417ab /test/regress/regress1 | |
| parent | 50c3dee5c8a4855023df826e1a733ea3c6076774 (diff) | |
[proof-new] Connecting new unsat cores (#5834)
Allows one to generate unsat cores from the new proof infrastructure. For new this is controlled by a new option, --check-unsat-cores-new.
Diffstat (limited to 'test/regress/regress1')
| -rw-r--r-- | test/regress/regress1/fmf/PUZ001+1.smt2 | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/test/regress/regress1/fmf/PUZ001+1.smt2 b/test/regress/regress1/fmf/PUZ001+1.smt2 index 607a79f0d..9c36ac561 100644 --- a/test/regress/regress1/fmf/PUZ001+1.smt2 +++ b/test/regress/regress1/fmf/PUZ001+1.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --finite-model-find --no-check-unsat-core +; COMMAND-LINE: --finite-model-find --no-check-unsat-cores ; EXPECT: unsat ;%------------------------------------------------------------------------------ ;% File : PUZ001+1 : TPTP v5.4.0. Released v2.0.0. @@ -53,7 +53,7 @@ (declare-fun richer__smt2_2 ( sort__smt2 sort__smt2 ) Bool) ; pel55_1 axiom -(assert (exists ((?X sort__smt2)) +(assert (exists ((?X sort__smt2)) (and (lives__smt2_1 ?X) (killed__smt2_2 ?X agatha__smt2_0)))) @@ -67,44 +67,44 @@ (assert (lives__smt2_1 charles__smt2_0)) ; pel55_3 axiom -(assert (forall ((?X sort__smt2)) +(assert (forall ((?X sort__smt2)) (=> (lives__smt2_1 ?X) (or (= ?X agatha__smt2_0) (= ?X butler__smt2_0) (= ?X charles__smt2_0))))) ; pel55_4 axiom -(assert (forall ((?X sort__smt2) (?Y sort__smt2)) +(assert (forall ((?X sort__smt2) (?Y sort__smt2)) (=> (killed__smt2_2 ?X ?Y) (hates__smt2_2 ?X ?Y)))) ; pel55_5 axiom -(assert (forall ((?X sort__smt2) (?Y sort__smt2)) +(assert (forall ((?X sort__smt2) (?Y sort__smt2)) (=> (killed__smt2_2 ?X ?Y) (not (richer__smt2_2 ?X ?Y))))) ; pel55_6 axiom -(assert (forall ((?X sort__smt2)) +(assert (forall ((?X sort__smt2)) (=> (hates__smt2_2 agatha__smt2_0 ?X) (not (hates__smt2_2 charles__smt2_0 ?X))))) ; pel55_7 axiom -(assert (forall ((?X sort__smt2)) +(assert (forall ((?X sort__smt2)) (=> (not (= ?X butler__smt2_0)) (hates__smt2_2 agatha__smt2_0 ?X)))) ; pel55_8 axiom -(assert (forall ((?X sort__smt2)) +(assert (forall ((?X sort__smt2)) (=> (not (richer__smt2_2 ?X agatha__smt2_0)) (hates__smt2_2 butler__smt2_0 ?X)))) ; pel55_9 axiom -(assert (forall ((?X sort__smt2)) +(assert (forall ((?X sort__smt2)) (=> (hates__smt2_2 agatha__smt2_0 ?X) (hates__smt2_2 butler__smt2_0 ?X)))) ; pel55_10 axiom -(assert (forall ((?X sort__smt2)) +(assert (forall ((?X sort__smt2)) (exists ((?Y sort__smt2)) (not (hates__smt2_2 ?X ?Y))))) ; pel55_11 axiom |