projects / cvc5.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: f66f409)
Fix regression requiring proof build. (#2364)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 23 Aug 2018 19:11:36 +0000 (14:11 -0500)
committerGitHub <noreply@github.com>
Thu, 23 Aug 2018 19:11:36 +0000 (14:11 -0500)
test/regress/regress1/quantifiers/dump-inst-proof.smt2 patch | blob | history

diff --git a/test/regress/regress1/quantifiers/dump-inst-proof.smt2 b/test/regress/regress1/quantifiers/dump-inst-proof.smt2
index c4eedc16f6bf085eb13f86107a7a7fa525527751..674950c34414e69f1ff3242ad2b98faa1bdb742d 100644 (file)
--- a/test/regress/regress1/quantifiers/dump-inst-proof.smt2
+++ b/test/regress/regress1/quantifiers/dump-inst-proof.smt2
@@ -1,3 +1,4 @@
+; REQUIRES: proof
 ; COMMAND-LINE: --dump-instantiations --proof
 ; EXPECT: unsat
 ; EXPECT: (instantiation (forall ((x Int)) (or (P x) (Q x)) )