From d580f2d380375953413ce1568ca30cd9b862af45 Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Sat, 2 Mar 2024 01:32:54 -0300 Subject: [PATCH] disabling define-fun-rec regressions --- test/regress/cli/regress1/quantifiers/const.cvc.smt2 | 2 ++ test/regress/cli/regress1/quantifiers/constfunc.cvc.smt2 | 2 ++ test/regress/cli/regress1/quantifiers/is-even.smt2 | 2 ++ test/regress/cli/regress1/quantifiers/mutualrec2.cvc.smt2 | 2 ++ test/regress/cli/regress1/quantifiers/recfact.cvc.smt2 | 2 ++ 5 files changed, 10 insertions(+) diff --git a/test/regress/cli/regress1/quantifiers/const.cvc.smt2 b/test/regress/cli/regress1/quantifiers/const.cvc.smt2 index 2f874925d9c..6616a37537e 100644 --- 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 index bd4e2eb9670..7e044574c21 100644 --- 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 index 0ccfff31fe1..17657edc4cb 100644 --- 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 index b9cd514a0dd..212a81d4e4f 100644 --- 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 index e367073602a..a2c59f816df 100644 --- 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)