From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 15 Apr 2021 19:08:00 +0000 (-0500)
Subject: Reenable regression for minimizing instantiations (#6367)
X-Git-Tag: cvc5-1.0.0~1898
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1bbcce82a9b8c122a0921a46265534e796047faa;p=cvc5.git

Reenable regression for minimizing instantiations (#6367)
---

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 710c06f96..a9b5174bb 100644
--- 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 0c8c21f01..c2ae56b88 100644
--- 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 )