From f55b23322860a8e186ae919daa4796ac4850a82e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 9 Apr 2022 12:06:39 +0200
Subject: [PATCH] #5778

---
 src/sat/smt/arith_solver.cpp  | 9 +++++----
 src/sat/smt/q_model_fixer.cpp | 6 ++++++
 2 files changed, 11 insertions(+), 4 deletions(-)

diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
index 5a102fa14..e02a42979 100644
--- a/src/sat/smt/arith_solver.cpp
+++ b/src/sat/smt/arith_solver.cpp
@@ -549,13 +549,14 @@ namespace arith {
         found_compatible = false;
         for (; it != end; ++it) {
             api_bound* a2 = *it;
-            if (a1 == a2) continue;
-            if (a2->get_bound_kind() != kind) continue;
+            if (a1 == a2)
+                continue;
+            if (a2->get_bound_kind() != kind)
+                continue;
             rational const& k2(a2->get_value());
             found_compatible = true;
-            if (k1 < k2) {
+            if (k1 < k2) 
                 return it;
-            }
         }
         return end;
     }
diff --git a/src/sat/smt/q_model_fixer.cpp b/src/sat/smt/q_model_fixer.cpp
index 456525c42..cdea60d23 100644
--- a/src/sat/smt/q_model_fixer.cpp
+++ b/src/sat/smt/q_model_fixer.cpp
@@ -184,6 +184,8 @@ namespace q {
         for (euf::enode* n : ctx.get_egraph().enodes_of(f)) {
             expr* t = n->get_arg(idx)->get_expr();
             values.push_back(mdl(t));
+            if (!m.is_value(values.back())) 
+                return expr_ref(m.mk_var(idx, srt), m);
             md->v2t.insert(values.back(), t);
             md->t2v.insert(t, values.back());
         }
@@ -299,6 +301,10 @@ namespace q {
         auto term = [&](unsigned j) {
             return md->v2t[md->values[j]];
         };
+        
+        for (unsigned j = 0; j < sz; ++j)
+            std::cout << mk_pp(md->values[j], m) << "\n";
+
 
         expr* arg = t->get_arg(i);