From a4354c960cfdb71fa1ff8e2fbc903c7a4a7e0113 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 3 Nov 2020 01:09:08 -0800
Subject: [PATCH] na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/smt/q_mbi.cpp | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/src/sat/smt/q_mbi.cpp b/src/sat/smt/q_mbi.cpp
index acbf1585d..04534ca6c 100644
--- a/src/sat/smt/q_mbi.cpp
+++ b/src/sat/smt/q_mbi.cpp
@@ -279,20 +279,31 @@ namespace q {
 
     /*
     * Remove occurrences of free functions that contain variables.
+    * Add top-level equalities for those occurrences.
+    * 
+    * F[g(t)] -> F[s] & g(t) = s
+    * 
+    * where 
+    * - eval(g(t)) = eval(s), 
+    * - t contains bound variables, 
+    * - s is ground.
     */
     void mbqi::eliminate_nested_vars(expr_ref_vector& fmls, q_body& qb) {
         if (qb.var_args.empty())
             return;
         expr_safe_replace rep(m);
         var_subst subst(m);
+        expr_ref_vector eqs(m);
         for (auto p : qb.var_args) {
             expr_ref _term = subst(p.first, qb.vars);
             app_ref  term(to_app(_term), m);
             expr_ref value = (*m_model)(term);
             expr* s = m_model_fixer.invert_app(term, value);
             rep.insert(term, s);
+            eqs.push_back(m.mk_eq(term, s));
         }
         rep(fmls);
+        fmls.append(eqs);
     }
 
     /*