From ec0b33514ffe0b8be065da424348cc1b1d06ecb6 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 25 Oct 2021 10:32:16 -0500 Subject: [PATCH] Reenable proofs on some regressions (#7483) --- test/regress/regress1/push-pop/arith_lra_01.smt2 | 2 +- test/regress/regress1/push-pop/fuzz_3_6.smt2 | 2 +- test/regress/regress1/quantifiers/symmetric_unsat_7.smt2 | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/test/regress/regress1/push-pop/arith_lra_01.smt2 b/test/regress/regress1/push-pop/arith_lra_01.smt2 index 02e22d685..b16bbdda0 100644 --- a/test/regress/regress1/push-pop/arith_lra_01.smt2 +++ b/test/regress/regress1/push-pop/arith_lra_01.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --incremental --no-produce-proofs +; COMMAND-LINE: --incremental ; EXPECT: sat ; EXPECT: sat ; EXPECT: sat diff --git a/test/regress/regress1/push-pop/fuzz_3_6.smt2 b/test/regress/regress1/push-pop/fuzz_3_6.smt2 index 4ad684402..1901016c2 100644 --- a/test/regress/regress1/push-pop/fuzz_3_6.smt2 +++ b/test/regress/regress1/push-pop/fuzz_3_6.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --incremental --no-produce-proofs +; COMMAND-LINE: --incremental ; EXPECT: sat ; EXPECT: sat ; EXPECT: unsat diff --git a/test/regress/regress1/quantifiers/symmetric_unsat_7.smt2 b/test/regress/regress1/quantifiers/symmetric_unsat_7.smt2 index 7249e87aa..465408cc5 100644 --- a/test/regress/regress1/quantifiers/symmetric_unsat_7.smt2 +++ b/test/regress/regress1/quantifiers/symmetric_unsat_7.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --no-check-unsat-cores --no-produce-proofs +; COMMAND-LINE: --no-check-unsat-cores ; EXPECT: unsat ; Note we require disabling proofs/unsat cores due to timeouts in nightlies -- 2.30.2