disabling define-fun-rec regressions

HanielB · Mar 2, 2024 · d580f2d · d580f2d
1 parent 4a98113
commit d580f2d
Show file tree

Hide file tree

Showing 5 changed files with 10 additions and 0 deletions.
diff --git a/test/regress/cli/regress1/quantifiers/const.cvc.smt2 b/test/regress/cli/regress1/quantifiers/const.cvc.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; defie-fun-rec not yet properly supported in Carcara
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-option :incremental false)
 (define-fun-rec five () Int 5)

diff --git a/test/regress/cli/regress1/quantifiers/constfunc.cvc.smt2 b/test/regress/cli/regress1/quantifiers/constfunc.cvc.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; defie-fun-rec not yet properly supported in Carcara
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-option :incremental false)
 (set-option :fmf-fun true)

diff --git a/test/regress/cli/regress1/quantifiers/is-even.smt2 b/test/regress/cli/regress1/quantifiers/is-even.smt2
@@ -1,3 +1,5 @@
+;; defie-fun-rec not yet properly supported in Carcara
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-info :status unsat)
 

diff --git a/test/regress/cli/regress1/quantifiers/mutualrec2.cvc.smt2 b/test/regress/cli/regress1/quantifiers/mutualrec2.cvc.smt2
@@ -1,4 +1,6 @@
 ; EXPECT: unsat
+;; defie-fun-rec not yet properly supported in Carcara
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-option :incremental false)
 (set-option :fmf-fun true)

diff --git a/test/regress/cli/regress1/quantifiers/recfact.cvc.smt2 b/test/regress/cli/regress1/quantifiers/recfact.cvc.smt2
@@ -4,6 +4,8 @@
 ;; The second command line option, other than the default, is to test
 ;; unsat core checking with proofs, which at one point had issues for
 ;; this benchmark due to cycle detection in LazyCDProofChain
+;; defie-fun-rec not yet properly supported in Carcara
+; DISABLE-TESTER: alethe
 (set-logic ALL)
 (set-option :incremental false)
 (set-option :fmf-fun true)