From: Andrew Reynolds Date: Thu, 23 Aug 2018 19:11:36 +0000 (-0500) Subject: Fix regression requiring proof build. (#2364) X-Git-Tag: cvc5-1.0.0~4733 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4dc48596188c0550e625434cdd893d909810f9de;p=cvc5.git Fix regression requiring proof build. (#2364) --- diff --git a/test/regress/regress1/quantifiers/dump-inst-proof.smt2 b/test/regress/regress1/quantifiers/dump-inst-proof.smt2 index c4eedc16f..674950c34 100644 --- 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)) )