diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 4379e3fe1..ab6249ff6 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -6315,11 +6315,11 @@ class Solver(Z3PPObject):
 
     def from_file(self, filename):
         """Parse assertions from a file"""
-        self.add([f for f in parse_smt2_file(filename)])
+        self.add([f for f in parse_smt2_file(filename, ctx=self.ctx)])
 
     def from_string(self, s):
         """Parse assertions from a string"""
-        self.add([f for f in parse_smt2_string(s)])
+        self.add([f for f in parse_smt2_string(s, ctx=self.ctx)])
         
     def assertions(self):
         """Return an AST vector containing all added constraints.
diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index 57ecc5bac..3942f96db 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/src/sat/sat_simplifier.cpp
@@ -1040,7 +1040,7 @@ namespace sat {
                     block_clause(c, l, new_entry);
                     s.m_num_blocked_clauses++;
                 }
-                s.unmark_all(c);                
+                s.unmark_all(c);
             }
             for (clause* c : m_to_remove) 
                 s.block_clause(*c);
@@ -1091,8 +1091,8 @@ namespace sat {
                     }
                     else {
                         unsigned j = 0;
-                        for (literal lit : inter) 
-                            if (c.contains(lit)) 
+                        for (literal lit : inter)
+                            if (c.contains(lit))
                                 inter[j++] = lit;
                         inter.shrink(j);
                         if (j == 0) return false;
@@ -1416,7 +1416,7 @@ namespace sat {
 
             clause_use_list & neg_occs = s.m_use_list.get(~l);
             clause_use_list::iterator it = neg_occs.mk_iterator();
-            for  (; !it.at_end(); it.next()) {
+            for (; !it.at_end(); it.next()) {
                 clause & c = it.curr();
                 if (c.is_blocked()) continue;
                 m_counter -= c.size();
diff --git a/src/sat/sat_simplifier_params.pyg b/src/sat/sat_simplifier_params.pyg
index 4cbd80788..6dd00ec83 100644
--- a/src/sat/sat_simplifier_params.pyg
+++ b/src/sat/sat_simplifier_params.pyg
@@ -22,6 +22,6 @@ def_module_params(module_name='sat',
                           ('resolution.cls_cutoff2', UINT, 700000000, 'limit2 - total number of problems clauses for the second cutoff of Boolean variable elimination'),
                           ('elim_vars', BOOL, True, 'enable variable elimination using resolution during simplification'),
                           ('elim_vars_bdd', BOOL, True, 'enable variable elimination using BDD recompilation during simplification'),
-	                  ('elim_vars_bdd_delay', UINT, 3, 'delay elimination of variables using BDDs until after simplification round'),
+                          ('elim_vars_bdd_delay', UINT, 3, 'delay elimination of variables using BDDs until after simplification round'),
                           ('subsumption', BOOL, True, 'eliminate subsumed clauses'),
                           ('subsumption.limit', UINT, 100000000, 'approx. maximum number of literals visited during subsumption (and subsumption resolution)')))