Reenable proofs on some regressions (#7483)

diff --git a/test/regress/regress1/push-pop/arith_lra_01.smt2 b/test/regress/regress1/push-pop/arith_lra_01.smt2
index 02e22d685e3da686026ab7691da97a64c0be1682..b16bbdda060a70d0f0b0c2569ae25332bef1b55a 100644 (file)
--- 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 4ad68440297b3674aec20f05b818b1ae4daf209e..1901016c2f4b557938fc04f9e26cb6e0764663c7 100644 (file)
--- 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 7249e87aa21d9634aff5f54a459695a61d73d02b..465408cc51c648ba6dff16da3bfcfa5a015a4a79 100644 (file)
--- 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