Reenable regression for minimizing instantiations (#6367)

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 710c06f969e3a91118ab73a45301e20339012053..a9b5174bb8aaa048be7890da16ef895ab396c4ee 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1736,6 +1736,7 @@ set(regress_1_tests
   regress1/quantifiers/constfunc.cvc
   regress1/quantifiers/dt-tc-opt-small.smt2
   regress1/quantifiers/dump-inst-i.smt2
+  regress1/quantifiers/dump-inst-proof.smt2
   regress1/quantifiers/dump-inst.smt2
   regress1/quantifiers/eqrange_ex_1.smt2
   regress1/quantifiers/ext-ex-deq-trigger.smt2
@@ -2559,8 +2560,6 @@ set(regression_disabled_tests
   regress1/quantifiers/anti-sk-simp.smt2
   # no longer support snorm option
   regress1/quantifiers/arith-snorm.smt2
-  # until we have support for minimizing instantiations based on unsat core
-  regress1/quantifiers/dump-inst-proof.smt2
   # ajreynol: different error messages on production and debug:
   regress1/quantifiers/macro-subtype-param.smt2
   # times out with competition build, ok with other builds:

diff --git a/test/regress/regress1/quantifiers/dump-inst-proof.smt2 b/test/regress/regress1/quantifiers/dump-inst-proof.smt2
index 0c8c21f01563e04b53a5bc282299a487df437be0..c2ae56b88655467f7af089c2ae22b5afca6aca90 100644 (file)
--- a/test/regress/regress1/quantifiers/dump-inst-proof.smt2
+++ b/test/regress/regress1/quantifiers/dump-inst-proof.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --dump-instantiations --produce-unsat-cores --print-inst-full
+; COMMAND-LINE: --dump-instantiations --produce-proofs --print-inst-full --no-check-unsat-cores
 ; EXPECT: unsat
 ; EXPECT: (instantiations (forall ((x Int)) (or (P x) (Q x)))
 ; EXPECT:   ( 2 )