Fix issues related to eliminating extended arithmetic operators (#5475)

This fixes 2 issues related to eliminating arithmetic operators:
(1) counterexample lemmas in CEGQI were not being preprocessed
(2) ensureLiteral was not doing term formula removal.
This corrects these two issues. Now ensureLiteral does full theory preprocessing on the term we are ensuring literal for, meaning this may trigger lemmas if the term contains extended arithmetic operators like div.

Fixes #5469, fixes #5470, fixes #5471.

This adds --sygus-inst to 2 of these benchmarks which moreover makes them solvable.

This also improves our assertions and trace messages.

1 files changed, 2 insertions, 1 deletions

diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index 3bf3cc425..561817aa8 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -603,7 +603,8 @@ void InstStrategyCegqi::registerCounterexampleLemma(Node q, Node lem)
     ce_vars.push_back(tutil->getInstantiationConstant(q, i));
   }
   CegInstantiator* cinst = getInstantiator(q);
-  LemmaStatus status = d_quantEngine->getOutputChannel().lemma(lem);
+  LemmaStatus status =
+      d_quantEngine->getOutputChannel().lemma(lem, LemmaProperty::PREPROCESS);
   Node ppLem = status.getRewrittenLemma();
   Trace("cegqi-debug") << "Counterexample lemma (post-preprocess): " << ppLem
                        << std::endl;