projects / cvc5.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: 5fa459b)
[Regressions] Require proof support for abduction (#3546)
authorAndres Noetzli <andres.noetzli@gmail.com>
Sun, 8 Dec 2019 19:56:50 +0000 (11:56 -0800)
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>
Sun, 8 Dec 2019 19:56:50 +0000 (13:56 -0600)
test/regress/regress1/sygus-abduct-test-ccore.smt2 patch | blob | history
test/regress/regress1/sygus/abd-simple-conj-4.smt2 patch | blob | history

diff --git a/test/regress/regress1/sygus-abduct-test-ccore.smt2 b/test/regress/regress1/sygus-abduct-test-ccore.smt2
index 86f5fe133995ca97a5d5449c65231fc06c7118df..adb38add05760925ce8499f30dc81775614a0047 100644 (file)
--- a/test/regress/regress1/sygus-abduct-test-ccore.smt2
+++ b/test/regress/regress1/sygus-abduct-test-ccore.smt2
@@ -1,3 +1,4 @@
+; REQUIRES: proof
 ; COMMAND-LINE: --produce-abducts --sygus-core-connective
 ; SCRUBBER: grep -v -E '(\(define-fun)'
 ; EXIT: 0
diff --git a/test/regress/regress1/sygus/abd-simple-conj-4.smt2 b/test/regress/regress1/sygus/abd-simple-conj-4.smt2
index 98bf70fd755eb24ebe3f0f1d05560525bd4dafed..dda5e9751c18d24a5805d6e2f84c6ce77521b922 100644 (file)
--- a/test/regress/regress1/sygus/abd-simple-conj-4.smt2
+++ b/test/regress/regress1/sygus/abd-simple-conj-4.smt2
@@ -1,3 +1,4 @@
+; REQUIRES: proof
 ; COMMAND-LINE: --produce-abducts --sygus-core-connective
 ; SCRUBBER: grep -v -E '(\(define-fun)'
 ; EXIT: 0