Fix models for sygus-inference, bv2int, real2int (#6421)

In each case, previously we were generating a define-fun, what we needed was to do a model substitution.

This actually meant that check-models was giving false positives. The model was incorrect but check-models succeeded due to its use of expand definitions.

1 files changed, 9 insertions, 0 deletions

diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp
index 22cc15a97..4be6b4aac 100644
--- a/src/preprocessing/preprocessing_pass_context.cpp
+++ b/src/preprocessing/preprocessing_pass_context.cpp
@@ -63,6 +63,15 @@ void PreprocessingPassContext::addModelSubstitution(const Node& lhs,
       lhs, d_smt->expandDefinitions(rhs, false));
 }
 
+void PreprocessingPassContext::addSubstitution(const Node& lhs,
+                                               const Node& rhs,
+                                               ProofGenerator* pg)
+{
+  d_topLevelSubstitutions.addSubstitution(lhs, rhs, pg);
+  // also add as a model substitution
+  addModelSubstitution(lhs, rhs);
+}
+
 ProofNodeManager* PreprocessingPassContext::getProofNodeManager()
 {
   return d_pnm;