From 721ce847f4d44fb7ee2509df3b34aad49fc7f484 Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Fri, 4 Sep 2020 19:06:03 -0300 Subject: [Regressions] Fix regression issues related to BV proofs (#5029) --- test/regress/regress1/sygus-abduct-test-user.smt2 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'test/regress/regress1/sygus-abduct-test-user.smt2') diff --git a/test/regress/regress1/sygus-abduct-test-user.smt2 b/test/regress/regress1/sygus-abduct-test-user.smt2 index fed9bd2a6..ed1d5c862 100644 --- a/test/regress/regress1/sygus-abduct-test-user.smt2 +++ b/test/regress/regress1/sygus-abduct-test-user.smt2 @@ -1,4 +1,4 @@ -; REQUIRES: proofs +; REQUIRES: proof ; COMMAND-LINE: --produce-abducts ; COMMAND-LINE: --produce-abducts --sygus-core-connective ; SCRUBBER: grep -v -E '(\(define-fun)' -- cgit v1.2.3