Improve getValue for non-evaluated operators (#6436)

This makes it so that we attempt evaluation + rewriting on applications of operators that do not always evaluate, and return constants in case the evaluation was successful.

This fixes warnings for check-models on 43 of our regressions, and also uncovered one regression where our model was wrong but check-models silently succeeded. I've opened CVC4/cvc4-projects#276 for fixing the latter.

13 files changed, 13 insertions, 13 deletions

diff --git a/test/regress/regress0/arith/div-chainable.smt2 b/test/regress/regress0/arith/div-chainable.smt2
index 90aca07c3..ac2fb2352 100644
--- a/test/regress/regress0/arith/div-chainable.smt2
+++ b/test/regress/regress0/arith/div-chainable.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: -q
+; COMMAND-LINE:
 ; EXPECT: sat
 (set-logic QF_NIA)
 (set-info :status sat)
diff --git a/test/regress/regress0/arith/issue3413.smt2 b/test/regress/regress0/arith/issue3413.smt2
index c871226ce..080b25cde 100644
--- a/test/regress/regress0/arith/issue3413.smt2
+++ b/test/regress/regress0/arith/issue3413.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: -q
+; COMMAND-LINE:
 ; EXPECT: sat
 (set-logic QF_NIA)
 (declare-fun a () Int)
diff --git a/test/regress/regress0/bug484.smt2 b/test/regress/regress0/bug484.smt2
index e4bac6a0a..ee7e18516 100644
--- a/test/regress/regress0/bug484.smt2
+++ b/test/regress/regress0/bug484.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: -q
+; COMMAND-LINE:
 ; EXPECT: sat
 
 ; Preamble  --------------
diff --git a/test/regress/regress0/bv/bv_to_int_5293_2.smt2 b/test/regress/regress0/bv/bv_to_int_5293_2.smt2
index 1f812a503..74cac0544 100644
--- a/test/regress/regress0/bv/bv_to_int_5293_2.smt2
+++ b/test/regress/regress0/bv/bv_to_int_5293_2.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: -q
+; COMMAND-LINE:
 ; EXPECT: sat
 (set-logic ALL)
 (set-option :solve-bv-as-int sum)
diff --git a/test/regress/regress0/decision/quant-ex1.smt2 b/test/regress/regress0/decision/quant-ex1.smt2
index 3bb3d5999..6fd9416d7 100644
--- a/test/regress/regress0/decision/quant-ex1.smt2
+++ b/test/regress/regress0/decision/quant-ex1.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --decision=justification -q
+; COMMAND-LINE: --decision=justification
 ; EXPECT: sat
 
 (set-logic AUFLIRA)
diff --git a/test/regress/regress0/fmf/QEpres-uf.855035.smtv1.smt2 b/test/regress/regress0/fmf/QEpres-uf.855035.smtv1.smt2
index 32a75e846..619779c78 100644
--- a/test/regress/regress0/fmf/QEpres-uf.855035.smtv1.smt2
+++ b/test/regress/regress0/fmf/QEpres-uf.855035.smtv1.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find -q
+; COMMAND-LINE: --finite-model-find
 ; EXPECT: sat
 (set-option :incremental false)
 (set-info :status sat)
diff --git a/test/regress/regress0/fmf/fmc_unsound_model.smt2 b/test/regress/regress0/fmf/fmc_unsound_model.smt2
index 5d0d8f6e6..e4e1f65b4 100644
--- a/test/regress/regress0/fmf/fmc_unsound_model.smt2
+++ b/test/regress/regress0/fmf/fmc_unsound_model.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find -q
+; COMMAND-LINE: --finite-model-find
 ; EXPECT: sat
 ; this problem produced a model where incorrectly card(a)=1 due to --mbqi=fmc
 (set-logic ALL_SUPPORTED)
diff --git a/test/regress/regress0/fmf/sc_bad_model_1221.smt2 b/test/regress/regress0/fmf/sc_bad_model_1221.smt2
index 890e765aa..d951e6c50 100644
--- a/test/regress/regress0/fmf/sc_bad_model_1221.smt2
+++ b/test/regress/regress0/fmf/sc_bad_model_1221.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find -q
+; COMMAND-LINE: --finite-model-find
 ; EXPECT: sat
 (set-logic ALL_SUPPORTED)
 (set-info :status sat)
diff --git a/test/regress/regress0/fp/issue3619.smt2 b/test/regress/regress0/fp/issue3619.smt2
index 3e0858035..55269e123 100644
--- a/test/regress/regress0/fp/issue3619.smt2
+++ b/test/regress/regress0/fp/issue3619.smt2
@@ -1,5 +1,5 @@
 ; REQUIRES: symfpu
-; COMMAND-LINE: -q
+; COMMAND-LINE:
 ; EXPECT: sat
 (set-logic QF_FPLRA)
 (set-info :status sat)
diff --git a/test/regress/regress0/push-pop/real-as-int-incremental.smt2 b/test/regress/regress0/push-pop/real-as-int-incremental.smt2
index 155033d7d..81af8c4e7 100644
--- a/test/regress/regress0/push-pop/real-as-int-incremental.smt2
+++ b/test/regress/regress0/push-pop/real-as-int-incremental.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --incremental --solve-real-as-int -q
+; COMMAND-LINE: --incremental --solve-real-as-int
 ; EXPECT: sat
 ; EXPECT: sat
 ; EXPECT: sat
diff --git a/test/regress/regress0/quantifiers/horn-ground-pre-post.smt2 b/test/regress/regress0/quantifiers/horn-ground-pre-post.smt2
index 3a4f24521..082df249b 100644
--- a/test/regress/regress0/quantifiers/horn-ground-pre-post.smt2
+++ b/test/regress/regress0/quantifiers/horn-ground-pre-post.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --sygus-inference -q
+; COMMAND-LINE: --sygus-inference
 ; EXPECT: sat
 (set-logic UFLIA)
 (set-info :status sat)
diff --git a/test/regress/regress0/quantifiers/issue2033-macro-arith.smt2 b/test/regress/regress0/quantifiers/issue2033-macro-arith.smt2
index d65a92aa5..7993910fd 100644
--- a/test/regress/regress0/quantifiers/issue2033-macro-arith.smt2
+++ b/test/regress/regress0/quantifiers/issue2033-macro-arith.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --macros-quant -q
+; COMMAND-LINE: --macros-quant
 ; EXPECT: sat
 (set-logic AUFNIRA)
 (set-info :status sat)
diff --git a/test/regress/regress0/quantifiers/macro-back-subs-sat.smt2 b/test/regress/regress0/quantifiers/macro-back-subs-sat.smt2
index bdb389a63..34b7422a5 100644
--- a/test/regress/regress0/quantifiers/macro-back-subs-sat.smt2
+++ b/test/regress/regress0/quantifiers/macro-back-subs-sat.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --macros-quant -q
+; COMMAND-LINE: --macros-quant
 ; EXPECT: sat
 (set-logic UFLIA)
 (declare-fun A (Int) Int)