diff --git a/src/sat/smt/q_mbi.cpp b/src/sat/smt/q_mbi.cpp
index ba6bc77b3..da6fe4191 100644
--- a/src/sat/smt/q_mbi.cpp
+++ b/src/sat/smt/q_mbi.cpp
@@ -169,9 +169,8 @@ namespace q {
                     return l_false;
                 if (check_forall_default(q, *qb, *mdl))
                     return l_false;
-                else {
-                    return l_undef;
-                }
+                else 
+                    return l_undef;                
             }
             if (m_generation_bound >= m_generation_max)
                 return l_true;
@@ -337,8 +336,8 @@ namespace q {
         qb.domain_eqs.reset();
         var_subst subst(m);
 
-        for (auto p : qb.var_args) {
-            expr_ref bounds = m_model_fixer.restrict_arg(p.first, p.second);  
+        for (auto [t, idx] : qb.var_args) {
+            expr_ref bounds = m_model_fixer.restrict_arg(t, idx);  
             if (m.is_true(bounds))
                 continue;
             expr_ref vbounds = subst(bounds, qb.vars);
@@ -393,11 +392,11 @@ namespace q {
         if (qb.var_args.empty())
             return;
         var_subst subst(m);
-        for (auto p : qb.var_args) {
-            expr_ref _term = subst(p.first, qb.vars);
+        for (auto [t, idx] : qb.var_args) {
+            expr_ref _term = subst(t, qb.vars);
             app_ref  term(to_app(_term), m);
-            expr_ref value = (*m_model)(term->get_arg(p.second));
-            m_model_fixer.invert_arg(term, p.second, value, qb.domain_eqs);
+            expr_ref value = (*m_model)(term->get_arg(idx));
+            m_model_fixer.invert_arg(term, idx, value, qb.domain_eqs);
         }
     }
 
diff --git a/src/sat/smt/q_model_fixer.cpp b/src/sat/smt/q_model_fixer.cpp
index c2defc71a..41b6f31fb 100644
--- a/src/sat/smt/q_model_fixer.cpp
+++ b/src/sat/smt/q_model_fixer.cpp
@@ -111,6 +111,18 @@ namespace q {
             add_projection_functions(mdl, f);
     }
 
+    /**
+    *  we are given f with interpretation:
+    *      if x = v0 and y = w0 then f0
+    *      else if x = v1 and y = w1 then f1
+    *      ...
+    * Create a new interpretation for f as follows:
+    * f := f_aux(project1(x), project2(y))
+    * f_aux uses the original interpretation of f
+    * project1 sorts the values of v0, v1, ..., and maps arguments below v0 to v0, between v0, v1 to v1 etc.
+    * project2 sorts values of w0, w1, ... and maps argument y to values w0, w1, ..
+    * 
+    */
     void model_fixer::add_projection_functions(model& mdl, func_decl* f) {
         // update interpretation of f so that the graph of f is fully determined by the
         // ground values of its arguments.