diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 523d40842..65f634b6b 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -482,6 +482,7 @@ def _to_ast_ref(a, ctx):
     else:
         return _to_expr_ref(a, ctx)
 
+
 #########################################
 #
 # Sorts
@@ -6664,17 +6665,11 @@ class Solver(Z3PPObject):
 
     def from_file(self, filename):
         """Parse assertions from a file"""
-        try:
-            Z3_solver_from_file(self.ctx.ref(), self.solver, filename)
-        except Z3Exception as e:
-            _handle_parse_error(e, self.ctx)
+        Z3_solver_from_file(self.ctx.ref(), self.solver, filename)
 
     def from_string(self, s):
         """Parse assertions from a string"""
-        try:
-           Z3_solver_from_string(self.ctx.ref(), self.solver, s)
-        except Z3Exception as e:
-            _handle_parse_error(e, self.ctx)        
+        Z3_solver_from_string(self.ctx.ref(), self.solver, s)
     
     def cube(self, vars = None):
         """Get set of cubes
@@ -7063,17 +7058,11 @@ class Fixedpoint(Z3PPObject):
 
     def parse_string(self, s):
         """Parse rules and queries from a string"""
-        try:
-            return AstVector(Z3_fixedpoint_from_string(self.ctx.ref(), self.fixedpoint, s), self.ctx)
-        except Z3Exception as e:
-            _handle_parse_error(e, self.ctx)
+        return AstVector(Z3_fixedpoint_from_string(self.ctx.ref(), self.fixedpoint, s), self.ctx)
 
     def parse_file(self, f):
         """Parse rules and queries from a file"""
-        try:
-            return AstVector(Z3_fixedpoint_from_file(self.ctx.ref(), self.fixedpoint, f), self.ctx)
-        except Z3Exception as e:
-            _handle_parse_error(e, self.ctx)
+        return AstVector(Z3_fixedpoint_from_file(self.ctx.ref(), self.fixedpoint, f), self.ctx)
 
     def get_rules(self):
         """retrieve rules that have been added to fixedpoint context"""
@@ -7410,17 +7399,11 @@ class Optimize(Z3PPObject):
 
     def from_file(self, filename):
         """Parse assertions and objectives from a file"""
-        try:
-            Z3_optimize_from_file(self.ctx.ref(), self.optimize, filename)
-        except Z3Exception as e:
-            _handle_parse_error(e, self.ctx)
+        Z3_optimize_from_file(self.ctx.ref(), self.optimize, filename)
 
     def from_string(self, s):
         """Parse assertions and objectives from a string"""
-        try:
-            Z3_optimize_from_string(self.ctx.ref(), self.optimize, s)
-        except Z3Exception as e:
-            _handle_parse_error(e, self.ctx)
+        Z3_optimize_from_string(self.ctx.ref(), self.optimize, s)
 
     def assertions(self):
         """Return an AST vector containing all added constraints."""
diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp
index 0271d8311..a7f6fb07b 100644
--- a/src/ast/datatype_decl_plugin.cpp
+++ b/src/ast/datatype_decl_plugin.cpp
@@ -143,7 +143,77 @@ namespace datatype {
             }
             return r;
         }
-        size* size::mk_power(size* a1, size* a2) { return alloc(power, a1, a2); }
+
+        size* size::mk_power(size* a1, size* a2) { 
+            return alloc(power, a1, a2); 
+        }
+
+        
+        sort_size plus::eval(obj_map<sort, sort_size> const& S) {
+            rational r(0);
+            ptr_vector<size> todo;
+            todo.push_back(m_arg1);
+            todo.push_back(m_arg2);
+            while (!todo.empty()) {
+                size* s = todo.back();
+                todo.pop_back();
+                plus* p = dynamic_cast<plus*>(s);
+                if (p) {
+                    todo.push_back(p->m_arg1);
+                    todo.push_back(p->m_arg2);
+                }
+                else {
+                    sort_size sz = s->eval(S);                        
+                    if (sz.is_infinite()) return sz;
+                    if (sz.is_very_big()) return sz;
+                    r += rational(sz.size(), rational::ui64());
+                }
+            }
+            return sort_size(r);
+        }
+
+        size* plus::subst(obj_map<sort,size*>& S) { 
+            return mk_plus(m_arg1->subst(S), m_arg2->subst(S)); 
+        }
+
+        sort_size times::eval(obj_map<sort, sort_size> const& S) {
+            sort_size s1 = m_arg1->eval(S);
+            sort_size s2 = m_arg2->eval(S);
+            if (s1.is_infinite()) return s1;
+            if (s2.is_infinite()) return s2;
+            if (s1.is_very_big()) return s1;
+            if (s2.is_very_big()) return s2;
+            rational r = rational(s1.size(), rational::ui64()) * rational(s2.size(), rational::ui64());
+            return sort_size(r);
+        }
+
+        size* times::subst(obj_map<sort,size*>& S) { 
+            return mk_times(m_arg1->subst(S), m_arg2->subst(S)); 
+        }
+
+        sort_size power::eval(obj_map<sort, sort_size> const& S) {
+            sort_size s1 = m_arg1->eval(S);
+            sort_size s2 = m_arg2->eval(S);
+            // s1^s2
+            if (s1.is_infinite()) return s1;
+            if (s2.is_infinite()) return s2;
+            if (s1.is_very_big()) return s1;
+            if (s2.is_very_big()) return s2;
+            if (s1.size() == 1) return s1;
+            if (s2.size() == 1) return s1;
+            if (s1.size() > (2 << 20) || s2.size() > 10) return sort_size::mk_very_big();
+            rational r = ::power(rational(s1.size(), rational::ui64()), static_cast<unsigned>(s2.size()));
+            return sort_size(r);
+        }
+
+        size* power::subst(obj_map<sort,size*>& S) { 
+            return mk_power(m_arg1->subst(S), m_arg2->subst(S)); 
+        }
+
+        size* sparam::subst(obj_map<sort, size*>& S) { 
+            return S[m_param]; 
+        }
+
     }
 
     namespace decl {
@@ -667,7 +737,7 @@ namespace datatype {
                 continue;
             }
 
-            ptr_vector<param_size::size> s_add;        
+            ptr_vector<param_size::size> s_add;      
             for (constructor const* c : d) {
                 ptr_vector<param_size::size> s_mul;
                 for (accessor const* a : *c) {
diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h
index fc98c97e7..16d1f74c0 100644
--- a/src/ast/datatype_decl_plugin.h
+++ b/src/ast/datatype_decl_plugin.h
@@ -132,71 +132,28 @@ namespace datatype {
             size* m_arg1, *m_arg2;
             plus(size* a1, size* a2): m_arg1(a1), m_arg2(a2) { a1->inc_ref(); a2->inc_ref();}
             ~plus() override { m_arg1->dec_ref(); m_arg2->dec_ref(); }
-            size* subst(obj_map<sort,size*>& S) override { return mk_plus(m_arg1->subst(S), m_arg2->subst(S)); }
-            sort_size eval(obj_map<sort, sort_size> const& S) override {
-                rational r(0);
-                ptr_vector<size> todo;
-                todo.push_back(m_arg1);
-                todo.push_back(m_arg2);
-                while (!todo.empty()) {
-                    size* s = todo.back();
-                    todo.pop_back();
-                    plus* p = dynamic_cast<plus*>(s);
-                    if (p) {
-                        todo.push_back(p->m_arg1);
-                        todo.push_back(p->m_arg2);
-                    }
-                    else {
-                        sort_size sz = s->eval(S);                        
-                        if (sz.is_infinite()) return sz;
-                        if (sz.is_very_big()) return sz;
-                        r += rational(sz.size(), rational::ui64());
-                    }
-                }
-                return sort_size(r);
-            }
+            size* subst(obj_map<sort,size*>& S) override;
+            sort_size eval(obj_map<sort, sort_size> const& S) override;
         };
         struct times : public size {
             size* m_arg1, *m_arg2;
             times(size* a1, size* a2): m_arg1(a1), m_arg2(a2) { a1->inc_ref(); a2->inc_ref(); }
             ~times() override { m_arg1->dec_ref(); m_arg2->dec_ref(); }
-            size* subst(obj_map<sort,size*>& S) override { return mk_times(m_arg1->subst(S), m_arg2->subst(S)); }
-            sort_size eval(obj_map<sort, sort_size> const& S) override {
-                sort_size s1 = m_arg1->eval(S);
-                sort_size s2 = m_arg2->eval(S);
-                if (s1.is_infinite()) return s1;
-                if (s2.is_infinite()) return s2;
-                if (s1.is_very_big()) return s1;
-                if (s2.is_very_big()) return s2;
-                rational r = rational(s1.size(), rational::ui64()) * rational(s2.size(), rational::ui64());
-                return sort_size(r);
-            }
+            size* subst(obj_map<sort,size*>& S) override;
+            sort_size eval(obj_map<sort, sort_size> const& S) override;
         };
         struct power : public size {
             size* m_arg1, *m_arg2;
             power(size* a1, size* a2): m_arg1(a1), m_arg2(a2) { a1->inc_ref(); a2->inc_ref(); }
             ~power() override { m_arg1->dec_ref(); m_arg2->dec_ref(); }
-            size* subst(obj_map<sort,size*>& S) override { return mk_power(m_arg1->subst(S), m_arg2->subst(S)); }
-            sort_size eval(obj_map<sort, sort_size> const& S) override {
-                sort_size s1 = m_arg1->eval(S);
-                sort_size s2 = m_arg2->eval(S);
-                // s1^s2
-                if (s1.is_infinite()) return s1;
-                if (s2.is_infinite()) return s2;
-                if (s1.is_very_big()) return s1;
-                if (s2.is_very_big()) return s2;
-                if (s1.size() == 1) return s1;
-                if (s2.size() == 1) return s1;
-                if (s1.size() > (2 << 20) || s2.size() > 10) return sort_size::mk_very_big();
-                rational r = ::power(rational(s1.size(), rational::ui64()), static_cast<unsigned>(s2.size()));
-                return sort_size(r);
-            }
+            size* subst(obj_map<sort,size*>& S) override;
+            sort_size eval(obj_map<sort, sort_size> const& S) override;
         };
         struct sparam : public size {
             sort_ref m_param;
             sparam(sort_ref& p): m_param(p) {}
             ~sparam() override {}
-            size* subst(obj_map<sort,size*>& S) override { return S[m_param]; }
+            size* subst(obj_map<sort, size*>& S) override;
             sort_size eval(obj_map<sort, sort_size> const& S) override { return S[m_param]; }
         };
     };
diff --git a/src/sat/sat_cleaner.cpp b/src/sat/sat_cleaner.cpp
index c0c6fabe4..e13a117fd 100644
--- a/src/sat/sat_cleaner.cpp
+++ b/src/sat/sat_cleaner.cpp
@@ -192,10 +192,14 @@ namespace sat {
         report rpt(*this);
         m_last_num_units = trail_sz;
         m_cleanup_counter = 0;
-        cleanup_watches();
-        cleanup_clauses(s.m_clauses);
-        cleanup_clauses(s.m_learned);
-        s.propagate(false);
+        do {
+            trail_sz = s.m_trail.size();
+            cleanup_watches();
+            cleanup_clauses(s.m_clauses);
+            cleanup_clauses(s.m_learned);
+            s.propagate(false);
+        }
+        while (trail_sz < s.m_trail.size());
         CASSERT("cleaner_bug", s.check_invariant());
         return true;
     }