diff --git a/contrib/get-carcara-checker b/contrib/get-carcara-checker index 43bf2f6f28b..cb16d6bbcd5 100755 --- a/contrib/get-carcara-checker +++ b/contrib/get-carcara-checker @@ -24,9 +24,10 @@ CARCARA_DIR="$BASE_DIR/carcara" mkdir -p $CARCARA_DIR # download and unpack Carcara -CARCARA_VERSION="e770994b5d981257d53a83d38a679fa98c144005" +CARCARA_VERSION="d434d5caa0f2dad65aaa9ac9c20817af53004088" download "https://github.com/hanielb/carcara/archive/$CARCARA_VERSION.tar.gz" $BASE_DIR/tmp/carcara.tgz tar --strip 1 -xzf $BASE_DIR/tmp/carcara.tgz -C $CARCARA_DIR +rm $BASE_DIR/tmp/carcara.tgz # build carcara pushd $CARCARA_DIR @@ -67,4 +68,4 @@ echo " $CVC_DIR/deps/bin/cvc5-alethe-proof.sh cvc5 " echo "Check a proof:" echo " $CVC_DIR/deps/bin/carcara-check.sh " echo "Run cvc5 and check the generated proof:" -echo " $CVC_DIR/deps/bin/cvc5-carcara-check.sh cvc5 " \ No newline at end of file +echo " $CVC_DIR/deps/bin/cvc5-carcara-check.sh cvc5 " diff --git a/test/regress/cli/regress0/bug1247.smt2 b/test/regress/cli/regress0/bug1247.smt2 index e73e42fb57e..7aca12c60d9 100644 --- a/test/regress/cli/regress0/bug1247.smt2 +++ b/test/regress/cli/regress0/bug1247.smt2 @@ -1,5 +1,7 @@ ; COMMAND-LINE: --incremental ; EXPECT: unsat +;; define-const is not supported in Alethe +; DISABLE-TESTER: alethe (set-logic QF_ABV) (set-info :status unsat) diff --git a/test/regress/cli/regress0/bv/issue9518.smt2 b/test/regress/cli/regress0/bv/issue9518.smt2 index ae3e683625e..9166fe37a06 100644 --- a/test/regress/cli/regress0/bv/issue9518.smt2 +++ b/test/regress/cli/regress0/bv/issue9518.smt2 @@ -1,3 +1,5 @@ +;; FP is not supported in Alethe +; DISABLE-TESTER: alethe (set-logic ALL) (set-info :status unsat) (set-option :bv-solver bitblast-internal) diff --git a/test/regress/cli/regress0/datatypes/stream-singleton.smt2 b/test/regress/cli/regress0/datatypes/stream-singleton.smt2 index 5ef10166238..fb4643abb04 100644 --- a/test/regress/cli/regress0/datatypes/stream-singleton.smt2 +++ b/test/regress/cli/regress0/datatypes/stream-singleton.smt2 @@ -1,3 +1,5 @@ +;; Codatatypes are not supported in Alethe +; DISABLE-TESTER: alethe (set-logic QF_ALL) (set-info :status unsat) diff --git a/test/regress/cli/regress0/proofs/issue10278-pf-clone.smt2 b/test/regress/cli/regress0/proofs/issue10278-pf-clone.smt2 index 4f0992bc30e..ac731135d03 100644 --- a/test/regress/cli/regress0/proofs/issue10278-pf-clone.smt2 +++ b/test/regress/cli/regress0/proofs/issue10278-pf-clone.smt2 @@ -3,6 +3,7 @@ ; DISABLE-TESTER: unsat-core ; DISABLE-TESTER: cpc ; DISABLE-TESTER: lfsc +; DISABLE-TESTER: alethe ; REQUIRES: no-competition ; SCRUBBER: grep -o "unsat" ; EXPECT: unsat diff --git a/test/regress/cli/regress0/proofs/proj-issue723-rdb-step.smt2 b/test/regress/cli/regress0/proofs/proj-issue723-rdb-step.smt2 index b2e0002e5cd..ddbc3bb29b3 100644 --- a/test/regress/cli/regress0/proofs/proj-issue723-rdb-step.smt2 +++ b/test/regress/cli/regress0/proofs/proj-issue723-rdb-step.smt2 @@ -1,4 +1,6 @@ ; EXPECT: unsat +;; The option below forces the granularity "dsl-rewrite", which leads to an Alethe proof with the operators @bv and @bvsize, where the former is applied to a non-constant argument. This is unsupported. +; DISABLE-TESTER: alethe (set-logic ALL) (declare-const x (_ BitVec 1)) (set-option :check-proof-steps true) diff --git a/test/regress/cli/regress0/proofs/proof-components.smt2 b/test/regress/cli/regress0/proofs/proof-components.smt2 index 98d2b51eddc..651f3688fc7 100644 --- a/test/regress/cli/regress0/proofs/proof-components.smt2 +++ b/test/regress/cli/regress0/proofs/proof-components.smt2 @@ -3,6 +3,7 @@ ; EXPECT: unsat ; DISABLE-TESTER: lfsc ; DISABLE-TESTER: cpc +; DISABLE-TESTER: alethe (set-logic QF_UFLIA) (set-info :smt-lib-version 2.0) (set-info :category "crafted") diff --git a/test/regress/cli/regress0/proofs/t1-difficulty-filter.smt2 b/test/regress/cli/regress0/proofs/t1-difficulty-filter.smt2 index a96685fea16..4e9818be73c 100644 --- a/test/regress/cli/regress0/proofs/t1-difficulty-filter.smt2 +++ b/test/regress/cli/regress0/proofs/t1-difficulty-filter.smt2 @@ -3,12 +3,13 @@ ; EXPECT: unsat ; DISABLE-TESTER: lfsc ; DISABLE-TESTER: cpc +; DISABLE-TESTER: alethe (set-logic UFLIA) -(declare-fun f (Int) Int) -(declare-fun g (Int) Int) +(declare-fun f (Int) Int) +(declare-fun g (Int) Int) (declare-fun h (Int) Int) -(declare-fun a () Int) -(declare-fun b () Int) +(declare-fun a () Int) +(declare-fun b () Int) (declare-fun c () Int) (assert (forall ((x Int)) (> (f x) 5))) (assert (forall ((x Int)) (> (h x) 0))) diff --git a/test/regress/cli/regress0/proofs/unused-def1.smt2 b/test/regress/cli/regress0/proofs/unused-def1.smt2 index 179d1bb9ccc..136611ec5ec 100644 --- a/test/regress/cli/regress0/proofs/unused-def1.smt2 +++ b/test/regress/cli/regress0/proofs/unused-def1.smt2 @@ -1,5 +1,6 @@ ; EXPECT: unsat - +;; define-const is not supported in Alethe +; DISABLE-TESTER: alethe (set-logic UF) (declare-const x Bool) (define-const p Bool x) diff --git a/test/regress/cli/regress0/proofs/unused-def2.smt2 b/test/regress/cli/regress0/proofs/unused-def2.smt2 index 8acceaae7e1..7fdff5d55d7 100644 --- a/test/regress/cli/regress0/proofs/unused-def2.smt2 +++ b/test/regress/cli/regress0/proofs/unused-def2.smt2 @@ -1,7 +1,8 @@ ; COMMAND-LINE: --proof-prune-input ; SCRUBBER: grep -E "define|unsat" ; EXPECT: unsat - +;; define-const is not supported in Alethe +; DISABLE-TESTER: alethe (set-logic UF) (declare-const x Bool) (define-const p Bool x) diff --git a/test/regress/cli/regress0/quantifiers/dd.ricart-ieval.smt2 b/test/regress/cli/regress0/quantifiers/dd.ricart-ieval.smt2 index 705c7aa9c84..2c4f189abc6 100644 --- a/test/regress/cli/regress0/quantifiers/dd.ricart-ieval.smt2 +++ b/test/regress/cli/regress0/quantifiers/dd.ricart-ieval.smt2 @@ -1,5 +1,7 @@ ; COMMAND-LINE: --ieval=use --term-db-mode=all ; EXPECT: unsat +;; Unary OR implicitly removed by cvc5 +; DISABLE-TESTER: alethe (set-logic ALL) (declare-const x9 Bool) (declare-fun p () Int) diff --git a/test/regress/cli/regress0/smtlib/issue4552.smt2 b/test/regress/cli/regress0/smtlib/issue4552.smt2 index 8fcfabd5e05..5aa33ca38e8 100644 --- a/test/regress/cli/regress0/smtlib/issue4552.smt2 +++ b/test/regress/cli/regress0/smtlib/issue4552.smt2 @@ -2,6 +2,8 @@ ; EXPECT: unsat ; EXPECT: unsat ; EXPECT: unsat +;; define-const is not supported in Alethe +; DISABLE-TESTER: alethe (set-logic UF) (set-option :global-declarations true) diff --git a/test/regress/cli/regress0/tptp/SYN000=2.smt2 b/test/regress/cli/regress0/tptp/SYN000=2.smt2 index 0a167b8d35a..4a0ab094293 100644 --- a/test/regress/cli/regress0/tptp/SYN000=2.smt2 +++ b/test/regress/cli/regress0/tptp/SYN000=2.smt2 @@ -1,3 +1,5 @@ +;; Input has to_int applied to an integer +; DISABLE-TESTER: alethe (set-logic ALL) (set-info :status unsat) (declare-sort $$unsorted 0) diff --git a/test/regress/cli/regress1/bv/divtest.smt2 b/test/regress/cli/regress1/bv/divtest.smt2 index af9e2ea1fea..57fe3bc2821 100644 --- a/test/regress/cli/regress1/bv/divtest.smt2 +++ b/test/regress/cli/regress1/bv/divtest.smt2 @@ -1,5 +1,7 @@ ; DISABLE-TESTER: lfsc ; DISABLE-TESTER: dsl-proof +;; slow conversion +; DISABLE-TESTER: alethe (set-logic QF_BV) (set-info :status unsat) (declare-fun x1 () (_ BitVec 12)) diff --git a/test/regress/cli/regress1/bv/incorrect1.smtv1.smt2 b/test/regress/cli/regress1/bv/incorrect1.smtv1.smt2 index 06ff3aa2723..8d7535ce401 100644 --- a/test/regress/cli/regress1/bv/incorrect1.smtv1.smt2 +++ b/test/regress/cli/regress1/bv/incorrect1.smtv1.smt2 @@ -1,4 +1,6 @@ ; DISABLE-TESTER: lfsc +;; slow conversion +; DISABLE-TESTER: alethe (set-option :incremental false) (set-info :status unsat) (set-logic QF_BV) diff --git a/test/regress/cli/regress1/bvdiv2.smt2 b/test/regress/cli/regress1/bvdiv2.smt2 index 251b76c0352..83806a18e4a 100644 --- a/test/regress/cli/regress1/bvdiv2.smt2 +++ b/test/regress/cli/regress1/bvdiv2.smt2 @@ -1,4 +1,6 @@ ; DISABLE-TESTER: lfsc +;; slow conversion +; DISABLE-TESTER: alethe (set-logic QF_AUFBVLIA) (set-info :smt-lib-version 2.6) (set-info :category "crafted") diff --git a/test/regress/cli/regress1/proofs/base-lfsc-treesize.smt2 b/test/regress/cli/regress1/proofs/base-lfsc-treesize.smt2 index 58d49f4a471..287a28f3e47 100644 --- a/test/regress/cli/regress1/proofs/base-lfsc-treesize.smt2 +++ b/test/regress/cli/regress1/proofs/base-lfsc-treesize.smt2 @@ -1,4 +1,6 @@ ; EXPECT: unsat +;; slow conversion +; DISABLE-TESTER: alethe (set-logic QF_UFLIRA) (declare-sort FArray 2) diff --git a/test/regress/cli/regress1/quantifiers/cee-npnt-dd.smt2 b/test/regress/cli/regress1/quantifiers/cee-npnt-dd.smt2 index b497ad688a7..af7335230ba 100644 --- a/test/regress/cli/regress1/quantifiers/cee-npnt-dd.smt2 +++ b/test/regress/cli/regress1/quantifiers/cee-npnt-dd.smt2 @@ -1,6 +1,8 @@ ; COMMAND-LINE: --ee-mode=distributed ; COMMAND-LINE: --ee-mode=central ; EXPECT: unsat +;; Unary AND is not supported in Alethe +; DISABLE-TESTER: alethe (set-logic ALL) (set-info :status unsat) (set-option :fmf-bound true) diff --git a/test/regress/cli/regress1/quantifiers/dd.binary_trees.adb_1105_16_loop_invariant_init_1.smt2 b/test/regress/cli/regress1/quantifiers/dd.binary_trees.adb_1105_16_loop_invariant_init_1.smt2 index 2253b8cde8c..c79325f78d9 100644 --- a/test/regress/cli/regress1/quantifiers/dd.binary_trees.adb_1105_16_loop_invariant_init_1.smt2 +++ b/test/regress/cli/regress1/quantifiers/dd.binary_trees.adb_1105_16_loop_invariant_init_1.smt2 @@ -1,5 +1,7 @@ ; COMMAND-LINE: -q ; EXPECT: unsat +;; Unary OR is not supported in Alethe +; DISABLE-TESTER: alethe (set-logic ALL) (declare-sort e 0) (declare-sort p 0) diff --git a/test/regress/cli/regress1/quantifiers/dd.bug812-ieval.smt2 b/test/regress/cli/regress1/quantifiers/dd.bug812-ieval.smt2 index 32bfd0cf343..76b3186403f 100644 --- a/test/regress/cli/regress1/quantifiers/dd.bug812-ieval.smt2 +++ b/test/regress/cli/regress1/quantifiers/dd.bug812-ieval.smt2 @@ -1,5 +1,7 @@ ; COMMAND-LINE: --enum-inst --ieval=use ; EXPECT: unsat +;; Unary AND is not supported in Alethe +; DISABLE-TESTER: alethe (set-logic ALL) (declare-fun p (Int) Int) (declare-fun H (Int Int Int) Int) diff --git a/test/regress/cli/regress1/quantifiers/ddatv-delta2.smt2 b/test/regress/cli/regress1/quantifiers/ddatv-delta2.smt2 index 7940927ec51..c9ae56da189 100644 --- a/test/regress/cli/regress1/quantifiers/ddatv-delta2.smt2 +++ b/test/regress/cli/regress1/quantifiers/ddatv-delta2.smt2 @@ -1,3 +1,5 @@ +;; Unary OR is not supported in Alethe +; DISABLE-TESTER: alethe (set-logic ALL) (set-info :status unsat) (declare-sort U 0) @@ -5,7 +7,7 @@ (declare-datatypes ((H 0)) (((M (h T))))) (declare-fun S (U Int) T) (declare-fun n () H) -(assert (and +(assert (and (not (b (o (or (b (o (or (b (o (or (b (o (= (t (S (vc (v (S (vc (v E)) 0))) (t E))) (t (S (vc (v (S (vc (v (h n))) 0))) (t E)))))))))))))))) (b (o (forall ((i Int)) (or (< i (t (u (R E E)))) (b (o (forall ((z Int)) (! (or (b (o (or (b (o (< (t (S (vc (v (S (vc (v (h n))) z))) (t E))) (t (S (vc (v (S (vc (v (h n))) 0))) (t (I i))))))))))) :qid id)))))))))) (check-sat) diff --git a/test/regress/cli/regress1/quantifiers/issue10346-ieval-index-conflict.smt2 b/test/regress/cli/regress1/quantifiers/issue10346-ieval-index-conflict.smt2 index c20184ff61f..ff2c1bfc331 100644 --- a/test/regress/cli/regress1/quantifiers/issue10346-ieval-index-conflict.smt2 +++ b/test/regress/cli/regress1/quantifiers/issue10346-ieval-index-conflict.smt2 @@ -1,4 +1,6 @@ ; EXPECT: unsat +;; Unary AND is not supported in Alethe +; DISABLE-TESTER: alethe (set-logic ALIA) (declare-fun j () Int) (declare-fun a () (Array Int Int)) diff --git a/test/regress/cli/regress1/quantifiers/issue3250-syg-inf-q.smt2 b/test/regress/cli/regress1/quantifiers/issue3250-syg-inf-q.smt2 index e2a19e57879..8422e64fd51 100644 --- a/test/regress/cli/regress1/quantifiers/issue3250-syg-inf-q.smt2 +++ b/test/regress/cli/regress1/quantifiers/issue3250-syg-inf-q.smt2 @@ -1,14 +1,16 @@ +;; Unary AND is not supported in Alethe +; DISABLE-TESTER: alethe (set-logic ALL) (set-info :status unsat) -(declare-fun a () Real) -(assert - (and - (and - (exists ((?b Real)) (forall ((?c Real)) (exists ((?d Real)) - (or (and (and (and (and (< (+ (+ (+ 0.0 (* 68.0 ?c)) 0.0) (* 33.0 a)) 0.0) (<= 0.0 2.0)) +(declare-fun a () Real) +(assert + (and + (and + (exists ((?b Real)) (forall ((?c Real)) (exists ((?d Real)) + (or (and (and (and (and (< (+ (+ (+ 0.0 (* 68.0 ?c)) 0.0) (* 33.0 a)) 0.0) (<= 0.0 2.0)) (or (<= 0.0 (+ (* (+ (* 55.0 ?d) 0.0) (* 49.0 ?b)) 0.0)))))))))) ) ) -) +) (check-sat) diff --git a/test/regress/cli/regress1/quantifiers/issue6642-em-types.smt2 b/test/regress/cli/regress1/quantifiers/issue6642-em-types.smt2 index 19dc1122759..72c0c0792a5 100644 --- a/test/regress/cli/regress1/quantifiers/issue6642-em-types.smt2 +++ b/test/regress/cli/regress1/quantifiers/issue6642-em-types.smt2 @@ -1,5 +1,7 @@ ; COMMAND-LINE: --full-saturate-quant ; EXPECT: unsat +;; Logic not supported in Alethe +; DISABLE-TESTER: alethe (set-logic ALL) (declare-fun b () String) (assert (forall ((c (Seq Int))) (exists ((a String)) (and (= 1 (seq.len c)) (not (= b a)))))) diff --git a/test/regress/cli/regress1/quantifiers/issue8410-vts-subtypes.smt2 b/test/regress/cli/regress1/quantifiers/issue8410-vts-subtypes.smt2 index 3a2905fd494..20e83321f2c 100644 --- a/test/regress/cli/regress1/quantifiers/issue8410-vts-subtypes.smt2 +++ b/test/regress/cli/regress1/quantifiers/issue8410-vts-subtypes.smt2 @@ -1,5 +1,7 @@ ; COMMAND-LINE: -i ; EXPECT: unsat +;; Unary OR is not supported in Alethe +; DISABLE-TESTER: alethe (set-logic ALL) (push) (assert (or (forall ((v Real)) (or (exists ((V Real)) (or (exists ((V Real)) (= 0 (mod (to_int v) (to_int (- v))))))))))) diff --git a/test/regress/cli/regress1/quantifiers/issue8456-2-syqi-ic.smt2 b/test/regress/cli/regress1/quantifiers/issue8456-2-syqi-ic.smt2 index 97a10086a4c..84ecb7d94e3 100644 --- a/test/regress/cli/regress1/quantifiers/issue8456-2-syqi-ic.smt2 +++ b/test/regress/cli/regress1/quantifiers/issue8456-2-syqi-ic.smt2 @@ -1,5 +1,7 @@ ; COMMAND-LINE: --sygus-inst ; EXPECT: unsat +;; Unary AND is not supported in Alethe +; DISABLE-TESTER: alethe (set-logic ALL) (assert (and (forall ((v (Array (_ BitVec 1) Bool))) (select v (_ bv0 1))))) (check-sat) diff --git a/test/regress/cli/regress1/quantifiers/qcft-smtlib3dbc51.smt2 b/test/regress/cli/regress1/quantifiers/qcft-smtlib3dbc51.smt2 index a0b17eb7840..c93a416ad26 100644 --- a/test/regress/cli/regress1/quantifiers/qcft-smtlib3dbc51.smt2 +++ b/test/regress/cli/regress1/quantifiers/qcft-smtlib3dbc51.smt2 @@ -1,5 +1,7 @@ ; COMMAND-LINE: --cbqi-tconstraint --ieval=off ; EXPECT: unsat +;; slow conversion +; DISABLE-TESTER: alethe ; DISABLE-TESTER: dsl-proof (set-logic AUFLIRA) (set-info :source |http://proval.lri.fr/why-benchmarks |) diff --git a/test/regress/cli/regress1/quantifiers/smtlibe99bbe.smt2 b/test/regress/cli/regress1/quantifiers/smtlibe99bbe.smt2 index c2c28478455..79e4a039cbe 100644 --- a/test/regress/cli/regress1/quantifiers/smtlibe99bbe.smt2 +++ b/test/regress/cli/regress1/quantifiers/smtlibe99bbe.smt2 @@ -1,5 +1,7 @@ ; COMMAND-LINE: --relevant-triggers ; EXPECT: unsat +;; slow conversion +; DISABLE-TESTER: alethe ; DISABLE-TESTER: dsl-proof (set-logic AUFLIRA) (set-info :status unsat) diff --git a/test/regress/cli/regress1/sets/insert_invariant_37_2.smt2 b/test/regress/cli/regress1/sets/insert_invariant_37_2.smt2 index a8f117062d1..fea4a0117dd 100644 --- a/test/regress/cli/regress1/sets/insert_invariant_37_2.smt2 +++ b/test/regress/cli/regress1/sets/insert_invariant_37_2.smt2 @@ -1,3 +1,5 @@ +;; Logic not supported in Alethe +; DISABLE-TESTER: alethe (set-option :print-success false) (set-logic AUFLIAFS) (set-info :status unsat) diff --git a/test/regress/cli/regress1/strings/issue6913.smt2 b/test/regress/cli/regress1/strings/issue6913.smt2 index c8de4349ac9..c8ee5aa6909 100644 --- a/test/regress/cli/regress1/strings/issue6913.smt2 +++ b/test/regress/cli/regress1/strings/issue6913.smt2 @@ -1,5 +1,9 @@ ; COMMAND-LINE: --strings-exp ; EXPECT: unsat +;; repeated assumption in local proof lead to confusion with +;; discharge. Disabling for now while the use of "discharge" is not +;; properly defined in Alethe +; DISABLE-TESTER: alethe (set-logic ALL) (declare-fun a () String) (assert diff --git a/test/regress/cli/run_regression.py b/test/regress/cli/run_regression.py index 521125cd4bb..1041f3e0dcf 100755 --- a/test/regress/cli/run_regression.py +++ b/test/regress/cli/run_regression.py @@ -294,6 +294,10 @@ def run_internal(self, benchmark_info): output, error = output.decode(), error.decode() exit_code = self.check_exit_status(EXIT_OK, exit_status, output, error, cvc5_args) + if re.match(r'^unsat\n\(error "Proof unsupported by Alethe:', output): + print_ok("OK") + return exit_code + if exit_code != EXIT_OK: return exit_code original_file = benchmark_info.benchmark_dir + '/' + benchmark_info.benchmark_basename @@ -511,6 +515,7 @@ def run_internal(self, benchmark_info): "abduct": AbductTester(), "dump": DumpTester(), "dsl-proof": DslProofTester(), + "alethe": AletheTester(), "cpc": CpcTester() }