diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index 393fff202..8bb0e00c3 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -101,9 +101,9 @@ namespace {
                 result->set_model_converter(mc0()->translate(translator));
 
             for (auto& [k, v] : m_name2assertion) {
-                expr* val = translator(k);
-                expr* key = translator(v);
-                result->assert_expr(val, key);
+                expr* fml = translator(v);
+                expr* ind = translator(k);
+                result->assert_expr(fml, ind);
             }
 
             return result;