diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp
index 9ad51aaf4..fc42acbb9 100644
--- a/src/api/api_solver.cpp
+++ b/src/api/api_solver.cpp
@@ -179,6 +179,7 @@ extern "C" {
         LOG_Z3_solver_from_file(c, s, file_name);
         char const* ext = get_extension(file_name);
         std::ifstream is(file_name);
+        init_solver(c, s);
         if (!is) {
             SET_ERROR_CODE(Z3_FILE_ACCESS_ERROR, nullptr);
         }
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 604d7fb4b..f8e2f9fe1 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1685,15 +1685,15 @@ public:
         for (auto const& ev : ex.m_explanation) {
             fmls.push_back(constraint2fml(ev.second));
         }        
-        expr_ref t(m);
-        t = term2expr(term);
-        if (upper) 
+        expr_ref t(term2expr(term), m);
+        if (upper) {
             fmls.push_back(m.mk_not(a.mk_ge(t, a.mk_numeral(k, true))));
-        else 
+        }
+        else {
             fmls.push_back(m.mk_not(a.mk_le(t, a.mk_numeral(k, true))));
+        }
         ast_pp_util visitor(m);
         visitor.collect(fmls);
-
         visitor.display_decls(out);
         visitor.display_asserts(out, fmls, true);
         out << "(check-sat)\n";