6 files changed, 7 insertions, 17 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 4de32a426..1a33ee3a5 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -622,7 +622,6 @@ set(regress_0_tests
   regress0/nl/very-easy-sat.smt2
   regress0/nl/very-simple-unsat.smt2
   regress0/options/invalid_dump.smt2
-  regress0/options/invalid_option_inc_proofs.smt2
   regress0/opt-abd-no-use.smt2
   regress0/parallel-let.smt2
   regress0/parser/as.smt2
@@ -872,7 +871,7 @@ set(regress_0_tests
   regress0/seq/seq-nth.smt2
   regress0/seq/seq-nth-uf.smt2
   regress0/seq/seq-nth-uf-z.smt2
-  regress0/seq/seq-nth-undef.smt2        
+  regress0/seq/seq-nth-undef.smt2
   regress0/seq/seq-rewrites.smt2
   regress0/sets/abt-min.smt2
   regress0/sets/abt-te-exh.smt2
diff --git a/test/regress/regress0/bug217.smt2 b/test/regress/regress0/bug217.smt2
index 30c87333e..4d2e828b5 100644
--- a/test/regress/regress0/bug217.smt2
+++ b/test/regress/regress0/bug217.smt2
@@ -1,4 +1,3 @@
-; COMMAND-LINE: --fewer-preprocessing-holes
 ; EXPECT: unsat
 (set-logic QF_UF)
 (set-info :status unsat)
diff --git a/test/regress/regress0/options/invalid_option_inc_proofs.smt2 b/test/regress/regress0/options/invalid_option_inc_proofs.smt2
deleted file mode 100644
index f63dbd27f..000000000
--- a/test/regress/regress0/options/invalid_option_inc_proofs.smt2
+++ /dev/null
@@ -1,6 +0,0 @@
-; REQUIRES: proof
-; COMMAND-LINE: --incremental --proof
-; EXPECT: (error "Error in option parsing: --incremental is not supported with proofs")
-; EXIT: 1
-(set-logic QF_BV)
-(check-sat)
diff --git a/test/regress/regress1/bv/bench_38.delta.smt2 b/test/regress/regress1/bv/bench_38.delta.smt2
index 760614348..3f809716a 100644
--- a/test/regress/regress1/bv/bench_38.delta.smt2
+++ b/test/regress/regress1/bv/bench_38.delta.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --fewer-preprocessing-holes --check-proof --quiet
+; COMMAND-LINE: --quiet
 ; EXPECT: unsat
 (set-logic QF_BV)
 (declare-fun x () (_ BitVec 4))
diff --git a/test/regress/regress1/non-fatal-errors.smt2 b/test/regress/regress1/non-fatal-errors.smt2
index 1e1865883..ec3d02927 100644
--- a/test/regress/regress1/non-fatal-errors.smt2
+++ b/test/regress/regress1/non-fatal-errors.smt2
@@ -2,11 +2,10 @@
 ; EXPECT: success
 ; EXPECT: success
 ; EXPECT: success
+; EXPECT: unsupported
 ; EXPECT: success
 ; EXPECT: success
 ; EXPECT: success
-; EXPECT: success
-; EXPECT: (error "")
 ; EXPECT: (error "")
 ; EXPECT: (error "")
 ; EXPECT: (error "")
@@ -22,7 +21,6 @@
 (declare-fun p () Bool)
 (get-unsat-core)
 (get-value (p))
-(get-proof)
 (get-model)
 (get-assignment)
 (assert true)
diff --git a/test/regress/regress1/quantifiers/dump-inst-proof.smt2 b/test/regress/regress1/quantifiers/dump-inst-proof.smt2
index 9edc4df2b..f900e78a9 100644
--- a/test/regress/regress1/quantifiers/dump-inst-proof.smt2
+++ b/test/regress/regress1/quantifiers/dump-inst-proof.smt2
@@ -1,5 +1,5 @@
 ; REQUIRES: proof
-; COMMAND-LINE: --dump-instantiations --proof --print-inst-full
+; COMMAND-LINE: --dump-instantiations --produce-unsat-cores --print-inst-full
 ; EXPECT: unsat
 ; EXPECT: (instantiations (forall ((x Int)) (or (P x) (Q x)) )
 ; EXPECT:   ( 2 )
@@ -21,7 +21,7 @@
 (assert (forall ((x Int)) (or (not (S x)) (not (Q x)))))
 (assert (and (not (R 0)) (not (R 10)) (not (S 1)) (not (P 2))))
 (assert (S 2))
-; This tests that --proof minimizes the instantiations printed out.
-; This regression should require only the 2 instantiations above, but
-; may try more.
+; This tests that --produce-unsat-cores minimizes the instantiations
+; printed out.  This regression should require only the 2
+; instantiations above, but may try more.
 (check-sat)