diff --git a/CMakeLists.txt b/CMakeLists.txt
index 5934b7c17..188d8dfde 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -254,6 +254,15 @@ elseif (CYGWIN)
 elseif (WIN32)
   message(STATUS "Platform: Windows")
   list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_WINDOWS")
+elseif (EMSCRIPTEN)
+  message(STATUS "Platform: Emscripten")
+  list(APPEND Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS
+    "-Os"
+    "-s ALLOW_MEMORY_GROWTH=1"
+    "-s ASSERTIONS=0"
+    "-s DISABLE_EXCEPTION_CATCHING=0"
+    "-s ERROR_ON_UNDEFINED_SYMBOLS=1"
+  )
 else()
   message(FATAL_ERROR "Platform \"${CMAKE_SYSTEM_NAME}\" not recognised")
 endif()
diff --git a/examples/python/mini_ic3.py b/examples/python/mini_ic3.py
index 048e8e518..b7b732459 100644
--- a/examples/python/mini_ic3.py
+++ b/examples/python/mini_ic3.py
@@ -394,76 +394,4 @@ test("data/horn2.smt2")
 test("data/horn3.smt2")
 test("data/horn4.smt2")
 test("data/horn5.smt2")
-test("data/horn6.smt2")
-
-
-
-"""
-# TBD: Quip variant of IC3
-
-must = True
-may = False
-
-class QGoal:
-    def __init__(self, cube, parent, level, must):
-        self.level = level
-        self.cube = cube
-        self.parent = parent
-        self.must = must
-
-class Quip(MiniIC3):
-
-    # prev & tras -> r', such that r' intersects with cube
-    def add_reachable(self, prev, cube):
-        s = fd_solver()
-        s.add(self.trans)
-        s.add(prev)
-        s.add(Or(cube))
-        is_sat = s.check()
-        assert is_sat == sat
-        m = s.model();
-        result = self.values2literals(m, cube)
-        assert result
-        self.reachable.add(result)
-
-    # A state s0 and level f0 such that
-    # not(s0) is f0-1 inductive
-    def quip_blocked(self, s0, f0):
-        self.push_heap(QGoal(self.next(s0), None, f0, must))
-        while self.goals:
-           f, g = heapq.heappop(self.goals)
-           sys.stdout.write("%d." % f)
-           sys.stdout.flush()
-           if f == 0:
-              if g.must:
-                 print("")
-                 return g
-              self.add_reachable(self.init, p.parent.cube)
-              continue
-
-        # TBD
-        return None
-
-                        
-    def run(self):
-        if not check_disjoint(self.init, self.bad):
-           return "goal is reached in initial state"
-        level = 0
-        while True:
-            inv = self.is_valid()
-            if inv is not None:
-                return inv
-            is_sat, cube = self.unfold()
-            if is_sat == unsat:
-               level += 1
-               print("Unfold %d" % level)
-               sys.stdout.flush()
-               self.add_solver()
-            elif is_sat == sat:
-               cex = self.quipie_blocked(cube, level)
-               if cex is not None:
-                  return cex
-            else:
-               return is_sat  
-
-"""
+# test("data/horn6.smt2") # takes long time to finish
diff --git a/examples/python/mini_quip.py b/examples/python/mini_quip.py
new file mode 100644
index 000000000..a10d5a334
--- /dev/null
+++ b/examples/python/mini_quip.py
@@ -0,0 +1,786 @@
+from z3 import *
+import heapq
+import numpy
+import time
+import random
+
+verbose = True
+
+# Simplistic (and fragile) converter from
+# a class of Horn clauses corresponding to
+# a transition system into a transition system
+# representation as <init, trans, goal>
+# It assumes it is given three Horn clauses
+# of the form:
+#  init(x) => Invariant(x)
+#  Invariant(x) and trans(x,x') => Invariant(x')
+#  Invariant(x) and goal(x) => Goal(x)
+# where Invariant and Goal are uninterpreted predicates
+
+class Horn2Transitions:
+    def __init__(self):
+        self.trans = True
+        self.init = True
+        self.inputs = []
+        self.goal = True
+        self.index = 0
+
+    def parse(self, file):
+        fp = Fixedpoint()
+        goals = fp.parse_file(file)
+        for r in fp.get_rules():
+            if not is_quantifier(r):
+                continue
+            b = r.body()
+            if not is_implies(b):
+                continue
+            f = b.arg(0)
+            g = b.arg(1)
+            if self.is_goal(f, g):
+                continue
+            if self.is_transition(f, g):
+                continue
+            if self.is_init(f, g):
+                continue
+
+    def is_pred(self, p, name):
+        return is_app(p) and p.decl().name() == name
+
+    def is_goal(self, body, head):
+        if not self.is_pred(head, "Goal"):
+            return False
+        pred, inv = self.is_body(body)
+        if pred is None:
+            return False
+        self.goal = self.subst_vars("x", inv, pred)
+        self.goal = self.subst_vars("i", self.goal, self.goal)
+        self.inputs += self.vars
+        self.inputs = list(set(self.inputs))
+        return True
+
+    def is_body(self, body):
+        if not is_and(body):
+            return None, None
+        fmls = [f for f in body.children() if self.is_inv(f) is None]
+        inv = None
+        for f in body.children():
+            if self.is_inv(f) is not None:
+                inv = f;
+                break
+        return And(fmls), inv
+
+    def is_inv(self, f):
+        if self.is_pred(f, "Invariant"):
+            return f
+        return None
+
+    def is_transition(self, body, head):
+        pred, inv0 = self.is_body(body)
+        if pred is None:
+            return False
+        inv1 = self.is_inv(head)
+        if inv1 is None:
+            return False
+        pred = self.subst_vars("x",  inv0, pred)
+        self.xs = self.vars
+        pred = self.subst_vars("xn", inv1, pred)
+        self.xns = self.vars
+        pred = self.subst_vars("i", pred, pred)
+        self.inputs += self.vars
+        self.inputs = list(set(self.inputs))
+        self.trans = pred
+        return True
+
+    def is_init(self, body, head):
+        for f in body.children():
+            if self.is_inv(f) is not None:
+               return False
+        inv = self.is_inv(head)
+        if inv is None:
+            return False
+        self.init = self.subst_vars("x", inv, body)
+        return True
+
+    def subst_vars(self, prefix, inv, fml):
+        subst = self.mk_subst(prefix, inv)
+        self.vars = [ v for (k,v) in subst ]
+        return substitute(fml, subst)
+
+    def mk_subst(self, prefix, inv):
+        self.index = 0
+        if self.is_inv(inv) is not None:
+            return [(f, self.mk_bool(prefix)) for f in inv.children()]
+        else:
+            vars = self.get_vars(inv)
+            return [(f, self.mk_bool(prefix)) for f in vars]
+
+    def mk_bool(self, prefix):
+        self.index += 1
+        return Bool("%s%d" % (prefix, self.index))
+
+    def get_vars(self, f, rs=[]):
+        if is_var(f):
+            return z3util.vset(rs + [f], str)
+        else:
+            for f_ in f.children():
+                rs = self.get_vars(f_, rs)
+            return z3util.vset(rs, str)
+
+# Produce a finite domain solver.
+# The theory QF_FD covers bit-vector formulas
+# and pseudo-Boolean constraints.
+# By default cardinality and pseudo-Boolean
+# constraints are converted to clauses. To override
+# this default for cardinality constraints
+# we set sat.cardinality.solver to True
+
+def fd_solver():
+    s = SolverFor("QF_FD")
+    s.set("sat.cardinality.solver", True)
+    return s
+
+
+# negate, avoid double negation
+def negate(f):
+    if is_not(f):
+        return f.arg(0)
+    else:
+        return Not(f)
+
+def cube2clause(cube):
+    return Or([negate(f) for f in cube])
+
+class State:
+    def __init__(self, s):
+        self.R = set([])
+        self.solver = s
+
+    def add(self, clause):
+        if clause not in self.R:
+           self.R |= { clause }
+           self.solver.add(clause)
+
+def is_seq(f):
+    return isinstance(f, list) or isinstance(f, tuple) or isinstance(f, AstVector)
+
+# Check if the initial state is bad
+def check_disjoint(a, b):
+    s = fd_solver()
+    s.add(a)
+    s.add(b)
+    return unsat == s.check()
+
+
+# Remove clauses that are subsumed
+def prune(R):
+    removed = set([])
+    s = fd_solver()
+    for f1 in R:
+        s.push()
+        for f2 in R:
+            if f2 not in removed:
+               s.add(Not(f2) if f1.eq(f2) else f2)
+        if s.check() == unsat:
+            removed |= { f1 }
+        s.pop()
+    return R - removed
+
+# Quip variant of IC3
+
+must = True
+may = False
+
+class QLemma:
+    def __init__(self, c):
+        self.cube = c
+        self.clause = cube2clause(c)
+        self.bad = False
+
+    def __hash__(self):
+        return hash(tuple(set(self.cube)))
+
+    def __eq__(self, qlemma2):
+        if set(self.cube) == set(qlemma2.cube) and self.bad == qlemma2.bad:
+            return True
+        else:
+            return False
+
+    def __ne__():
+        if not self.__eq__(self, qlemma2):
+            return True
+        else:
+            return False
+
+
+class QGoal:
+    def __init__(self, cube, parent, level, must, encounter):
+        self.level = level
+        self.cube = cube
+        self.parent = parent
+        self.must = must
+
+    def __lt__(self, other):
+        return self.level < other.level
+
+
+class QReach:
+
+    # it is assumed that there is a single initial state
+    # with all latches set to 0 in hardware design, so
+    # here init will always give a state where all variable are set to 0
+    def __init__(self, init, xs):
+        self.xs = xs
+        self.constant_xs = [Not(x) for x in self.xs]
+        s = fd_solver()
+        s.add(init)
+        is_sat = s.check()
+        assert is_sat == sat
+        m = s.model()
+        # xs is a list, "for" will keep the order when iterating
+        self.states = numpy.array([[False for x in self.xs]])  # all set to False
+        assert not numpy.max(self.states)  # since all element is False, so maximum should be False
+
+    # check if new state exists
+    def is_exist(self, state):
+        if state in self.states:
+            return True
+        return False
+
+    def enumerate(self, i, state_b, state):
+        while i < len(state) and state[i] not in self.xs:
+            i += 1
+        if i >= len(state):
+            if state_b.tolist() not in self.states.tolist():
+                self.states = numpy.append(self.states, [state_b], axis = 0)
+                return state_b
+            else:
+                return None
+        state_b[i] = False
+        if self.enumerate(i+1, state_b, state) is not None:
+            return state_b
+        else:
+            state_b[i] = True
+            return self.enumerate(i+1, state_b, state)
+
+    def is_full_state(self, state):
+        for i in range(len(self.xs)):
+            if state[i] in self.xs:
+                return False
+        return True
+
+    def add(self, cube):
+        state = self.cube2partial_state(cube)
+        assert len(state) == len(self.xs)
+        if not self.is_exist(state):
+            return None
+        if self.is_full_state(state):
+            self.states = numpy.append(self.states, [state], axis = 0)
+        else:
+            # state[i] is instance, state_b[i] is boolean
+            state_b = numpy.array(state)
+            for i in range(len(state)):  # state is of same length as self.xs
+                # i-th literal in state hasn't been assigned value
+                # init un-assigned literals in state_b as True
+                # make state_b only contain boolean value
+                if state[i] in self.xs:
+                    state_b[i] = True
+                else:
+                    state_b[i] = is_true(state[i])
+            if self.enumerate(0, state_b, state) is not None:
+                lits_to_remove = set([negate(f) for f in list(set(cube) - set(self.constant_xs))])
+                self.constant_xs = list(set(self.constant_xs) - lits_to_remove)
+                return state
+        return None
+
+
+    def cube2partial_state(self, cube):
+        s = fd_solver()
+        s.add(And(cube))
+        is_sat = s.check()
+        assert is_sat == sat
+        m = s.model()
+        state = numpy.array([m.eval(x) for x in self.xs])
+        return state
+
+
+    def state2cube(self, s):
+        result = copy.deepcopy(self.xs)  # x1, x2, ...
+        for i in range(len(self.xs)):
+            if not s[i]:
+                result[i] = Not(result[i])
+        return result
+
+    def intersect(self, cube):
+        state = self.cube2partial_state(cube)
+        mask = True
+        for i in range(len(self.xs)):
+            if is_true(state[i]) or is_false(state[i]):
+                mask = (self.states[:, i] == state[i]) & mask
+        intersects = numpy.reshape(self.states[mask], (-1, len(self.xs)))
+        if intersects.size > 0:
+            return And(self.state2cube(intersects[0]))  # only need to return one single intersect
+        return None
+
+
+class Quip:
+
+    def __init__(self, init, trans, goal, x0, inputs, xn):
+        self.x0 = x0
+        self.inputs = inputs
+        self.xn = xn
+        self.init = init
+        self.bad = goal
+        self.trans = trans
+        self.min_cube_solver = fd_solver()
+        self.min_cube_solver.add(Not(trans))
+        self.goals = []
+        s = State(fd_solver())
+        s.add(init)
+        s.solver.add(trans)  # check if a bad state can be reached in one step from current level
+        self.states = [s]
+        self.s_bad = fd_solver()
+        self.s_good = fd_solver()
+        self.s_bad.add(self.bad)
+        self.s_good.add(Not(self.bad))
+        self.reachable = QReach(self.init, x0)
+        self.frames = []  # frames is a 2d list, each row (representing level) is a set containing several (clause, bad) pairs
+        self.count_may = 0
+
+    def next(self, f):
+        if is_seq(f):
+           return [self.next(f1) for f1 in f]
+        return substitute(f, zip(self.x0, self.xn))
+
+    def prev(self, f):
+        if is_seq(f):
+           return [self.prev(f1) for f1 in f]
+        return substitute(f, zip(self.xn, self.x0))
+
+    def add_solver(self):
+        s = fd_solver()
+        s.add(self.trans)
+        self.states += [State(s)]
+
+    def R(self, i):
+        return And(self.states[i].R)
+
+    def value2literal(self, m, x):
+        value = m.eval(x)
+        if is_true(value):
+            return x
+        if is_false(value):
+            return Not(x)
+        return None
+
+    def values2literals(self, m, xs):
+        p = [self.value2literal(m, x) for x in xs]
+        return [x for x in p if x is not None]
+
+    def project0(self, m):
+        return self.values2literals(m, self.x0)
+
+    def projectI(self, m):
+        return self.values2literals(m, self.inputs)
+
+    def projectN(self, m):
+        return self.values2literals(m, self.xn)
+
+
+    # Block a cube by asserting the clause corresponding to its negation
+    def block_cube(self, i, cube):
+        self.assert_clause(i, cube2clause(cube))
+
+    # Add a clause to levels 1 until i
+    def assert_clause(self, i, clause):
+        for j in range(1, i + 1):
+            self.states[j].add(clause)
+            assert str(self.states[j].solver) != str([False])
+
+
+    # minimize cube that is core of Dual solver.
+    # this assumes that props & cube => Trans
+    # which means props & cube can only give us a Tr in Trans,
+    # and it will never make !Trans sat
+    def minimize_cube(self, cube, inputs, lits):
+        # min_cube_solver has !Trans (min_cube.solver.add(!Trans))
+        is_sat = self.min_cube_solver.check(lits + [c for c in cube] + [i for i in inputs])
+        assert is_sat == unsat
+        # unsat_core gives us some lits which make Tr sat,
+        # so that we can ignore other lits and include more states
+        core = self.min_cube_solver.unsat_core()
+        assert core
+        return [c for c in core if c in set(cube)]
+
+    # push a goal on a heap
+    def push_heap(self, goal):
+        heapq.heappush(self.goals, (goal.level, goal))
+
+
+    # make sure cube to be blocked excludes all reachable states
+    def check_reachable(self, cube):
+        s = fd_solver()
+        for state in self.reachable.states:
+            s.push()
+            r = self.reachable.state2cube(state)
+            s.add(And(self.prev(r)))
+            s.add(self.prev(cube))
+            is_sat = s.check()
+            s.pop()
+            if is_sat == sat:
+                # if sat, it means the cube to be blocked contains reachable states
+                # so it is an invalid cube
+                return False
+        # if all fail, is_sat will be unsat
+        return True
+
+    # Rudimentary generalization:
+    # If the cube is already unsat with respect to transition relation
+    # extract a core (not necessarily minimal)
+    # otherwise, just return the cube.
+    def generalize(self, cube, f):
+        s = self.states[f - 1].solver
+        if unsat == s.check(cube):
+            core = s.unsat_core()
+            if self.check_reachable(core):
+                return core, f
+        return cube, f
+
+
+    def valid_reachable(self, level):
+        s = fd_solver()
+        s.add(self.init)
+        for i in range(level):
+            s.add(self.trans)
+        for state in self.reachable.states:
+            s.push()
+            s.add(And(self.next(self.reachable.state2cube(state))))
+            print self.reachable.state2cube(state)
+            print s.check()
+            s.pop()
+
+    def lemmas(self, level):
+        return [(l.clause, l.bad) for l in self.frames[level]]
+
+    # whenever a new reachable state is found, we use it to mark some existing lemmas as bad lemmas
+    def mark_bad_lemmas(self, new):
+        s = fd_solver()
+        reset = False
+        for frame in self.frames:
+            for lemma in frame:
+                s.push()
+                s.add(lemma.clause)
+                is_sat = s.check(new)
+                if is_sat == unsat:
+                    reset = True
+                    lemma.bad = True
+                s.pop()
+        if reset:
+            self.states = [self.states[0]]
+            for i in range(1, len(self.frames)):
+                self.add_solver()
+                for lemma in self.frames[i]:
+                    if not lemma.bad:
+                        self.states[i].add(lemma.clause)
+
+    # prev & tras -> r', such that r' intersects with cube
+    def add_reachable(self, prev, cube):
+        s = fd_solver()
+        s.add(self.trans)
+        s.add(prev)
+        s.add(self.next(And(cube)))
+        is_sat = s.check()
+        assert is_sat == sat
+        m = s.model()
+        new = self.projectN(m)
+        state = self.reachable.add(self.prev(new))  # always add as non-primed
+        if state is not None:  # if self.states do not have new state yet
+            self.mark_bad_lemmas(self.prev(new))
+
+
+    # Check if the negation of cube is inductive at level f
+    def is_inductive(self, f, cube):
+        s = self.states[f - 1].solver
+        s.push()
+        s.add(self.prev(Not(And(cube))))
+        is_sat = s.check(cube)
+        if is_sat == sat:
+            m = s.model()
+        s.pop()
+        if is_sat == sat:
+            cube = self.next(self.minimize_cube(self.project0(m), self.projectI(m), self.projectN(m)))
+        elif is_sat == unsat:
+            cube, f = self.generalize(cube, f)
+            cube = self.next(cube)
+        return cube, f, is_sat
+
+
+    # Determine if there is a cube for the current state
+    # that is potentially reachable.
+    def unfold(self, level):
+        core = []
+        self.s_bad.push()
+        R = self.R(level)
+        self.s_bad.add(R)  # check if current frame intersects with bad states, no trans
+        is_sat = self.s_bad.check()
+        if is_sat == sat:
+           m = self.s_bad.model()
+           cube = self.project0(m)
+           props = cube + self.projectI(m)
+           self.s_good.push()
+           self.s_good.add(R)
+           is_sat2 = self.s_good.check(props)
+           assert is_sat2 == unsat
+           core = self.s_good.unsat_core()
+           assert core
+           core = [c for c in core if c in set(cube)]
+           self.s_good.pop()
+        self.s_bad.pop()
+        return is_sat, core
+
+    # A state s0 and level f0 such that
+    # not(s0) is f0-1 inductive
+    def quip_blocked(self, s0, f0):
+        self.push_heap(QGoal(self.next(s0), None, f0, must, 0))
+        while self.goals:
+            f, g = heapq.heappop(self.goals)
+            sys.stdout.write("%d." % f)
+            if not g.must:
+                self.count_may -= 1
+            sys.stdout.flush()
+            if f == 0:
+                if g.must:
+                    s = fd_solver()
+                    s.add(self.init)
+                    s.add(self.prev(g.cube))
+                    # since init is a complete assignment, so g.cube must equal to init in sat solver
+                    assert is_sat == s.check()
+                    if verbose:
+                        print("")
+                    return g
+                self.add_reachable(self.init, g.parent.cube)
+                continue
+
+            r0 = self.reachable.intersect(self.prev(g.cube))
+            if r0 is not None:
+                if g.must:
+                    if verbose:
+                        print ""
+                    s = fd_solver()
+                    s.add(self.trans)
+                    # make it as a concrete reachable state
+                    # intersect returns an And(...), so use children to get cube list
+                    g.cube = r0.children()
+                    while True:
+                        is_sat = s.check(self.next(g.cube))
+                        assert is_sat == sat
+                        r = self.next(self.project0(s.model()))
+                        r = self.reachable.intersect(self.prev(r))
+                        child = QGoal(self.next(r.children()), g, 0, g.must, 0)
+                        g = child
+                        if not check_disjoint(self.init, self.prev(g.cube)):
+                            # g is init, break the loop
+                            break
+                    init = g
+                    while g.parent is not None:
+                        g.parent.level = g.level + 1
+                        g = g.parent
+                    return init
+                if g.parent is not None:
+                    self.add_reachable(r0, g.parent.cube)
+                continue
+
+            cube = None
+            is_sat = sat
+            f_1 = len(self.frames) - 1
+            while f_1 >= f:
+                for l in self.frames[f_1]:
+                    if not l.bad and len(l.cube) > 0 and set(l.cube).issubset(g.cube):
+                        cube = l.cube
+                        is_sat == unsat
+                        break
+                f_1 -= 1
+            if cube is None:
+                cube, f_1, is_sat = self.is_inductive(f, g.cube)
+            if is_sat == unsat:
+                self.frames[f_1].add(QLemma(self.prev(cube)))
+                self.block_cube(f_1, self.prev(cube))
+                if f_1 < f0:
+                    # learned clause might also be able to block same bad states in higher level
+                    if set(list(cube)) != set(list(g.cube)):
+                        self.push_heap(QGoal(cube, None, f_1 + 1, may, 0))
+                        self.count_may += 1
+                    else:
+                        # re-queue g.cube in higher level, here g.parent is simply for tracking down the trace when output.
+                        self.push_heap(QGoal(g.cube, g.parent, f_1 + 1, g.must, 0))
+                        if not g.must:
+                            self.count_may += 1
+            else:
+                # qcube is a predecessor of g
+                qcube = QGoal(cube, g, f_1 - 1, g.must, 0)
+                if not g.must:
+                    self.count_may += 1
+                self.push_heap(qcube)
+
+        if verbose:
+            print("")
+        return None
+
+    # Check if there are two states next to each other that have the same clauses.
+    def is_valid(self):
+        i = 1
+        inv = None
+        while True:
+            # self.states[].R contains full lemmas
+            # self.frames[] contains delta-encoded lemmas
+            while len(self.states) <= i+1:
+                self.add_solver()
+            while len(self.frames) <= i+1:
+                self.frames.append(set())
+            duplicates = set([])
+            for l in self.frames[i+1]:
+                if l in self.frames[i]:
+                    duplicates |= {l}
+            self.frames[i] = self.frames[i] - duplicates
+            pushed = set([])
+            for l in (self.frames[i] - self.frames[i+1]):
+                if not l.bad:
+                    s = self.states[i].solver
+                    s.push()
+                    s.add(self.next(Not(l.clause)))
+                    s.add(l.clause)
+                    is_sat = s.check()
+                    s.pop()
+                    if is_sat == unsat:
+                        self.frames[i+1].add(l)
+                        self.states[i+1].add(l.clause)
+                        pushed |= {l}
+            self.frames[i] = self.frames[i] - pushed
+            if (not (self.states[i].R - self.states[i+1].R)
+                and len(self.states[i].R) != 0):
+                inv = prune(self.states[i].R)
+                F_inf = self.frames[i]
+                j = i + 1
+                while j < len(self.states):
+                    for l in F_inf:
+                        self.states[j].add(l.clause)
+                    j += 1
+                self.frames[len(self.states)-1] = F_inf
+                self.frames[i] = set([])
+                break
+            elif (len(self.states[i].R) == 0
+                  and len(self.states[i+1].R) == 0):
+                break
+            i += 1
+
+        if inv is not None:
+            self.s_bad.push()
+            self.s_bad.add(And(inv))
+            is_sat = self.s_bad.check()
+            if is_sat == unsat:
+                self.s_bad.pop()
+                return And(inv)
+            self.s_bad.pop()
+        return None
+
+    def run(self):
+        if not check_disjoint(self.init, self.bad):
+            return "goal is reached in initial state"
+        level = 0
+        while True:
+            inv = self.is_valid()  # self.add_solver() here
+            if inv is not None:
+                return inv
+            is_sat, cube = self.unfold(level)
+            if is_sat == unsat:
+                level += 1
+                if verbose:
+                    print("Unfold %d" % level)
+                sys.stdout.flush()
+            elif is_sat == sat:
+                cex = self.quip_blocked(cube, level)
+                if cex is not None:
+                    return cex
+            else:
+                return is_sat
+
+def test(file):
+    h2t = Horn2Transitions()
+    h2t.parse(file)
+    if verbose:
+        print("Test file: %s") % file
+    mp = Quip(h2t.init, h2t.trans, h2t.goal, h2t.xs, h2t.inputs, h2t.xns)
+    start_time = time.time()
+    result = mp.run()
+    end_time = time.time()
+    if isinstance(result, QGoal):
+        g = result
+        if verbose:
+            print("Trace")
+        while g:
+           if verbose:
+               print(g.level, g.cube)
+           g = g.parent
+        print("--- used %.3f seconds ---" % (end_time - start_time))
+        validate(mp, result, mp.trans)
+        return
+    if isinstance(result, ExprRef):
+        if verbose:
+            print("Invariant:\n%s " % result)
+        print("--- used %.3f seconds ---" % (end_time - start_time))
+        validate(mp, result, mp.trans)
+        return
+    print(result)
+
+def validate(var, result, trans):
+    if isinstance(result, QGoal):
+        g = result
+        s = fd_solver()
+        s.add(trans)
+        while g.parent is not None:
+            s.push()
+            s.add(var.prev(g.cube))
+            s.add(var.next(g.parent.cube))
+            assert sat == s.check()
+            s.pop()
+            g = g.parent
+        if verbose:
+            print "--- validation succeed ----"
+        return
+    if isinstance(result, ExprRef):
+        inv = result
+        s = fd_solver()
+        s.add(trans)
+        s.push()
+        s.add(var.prev(inv))
+        s.add(Not(var.next(inv)))
+        assert unsat == s.check()
+        s.pop()
+        cube = var.prev(var.init)
+        step = 0
+        while True:
+            step += 1
+            # too many steps to reach invariant
+            if step > 1000:
+                if verbose:
+                    print "--- validation failed --"
+                return
+            if not check_disjoint(var.prev(cube), var.prev(inv)):
+                # reach invariant
+                break
+            s.push()
+            s.add(cube)
+            assert s.check() == sat
+            cube = var.projectN(s.model())
+            s.pop()
+        if verbose:
+            print "--- validation succeed ----"
+        return
+
+
+
+test("data/horn1.smt2")
+test("data/horn2.smt2")
+test("data/horn3.smt2")
+test("data/horn4.smt2")
+test("data/horn5.smt2")
+# test("data/horn6.smt2")  # not able to finish
diff --git a/scripts/mk_genfile_common.py b/scripts/mk_genfile_common.py
index a65b41026..6354613fe 100644
--- a/scripts/mk_genfile_common.py
+++ b/scripts/mk_genfile_common.py
@@ -8,6 +8,7 @@
 # You should **not** import ``mk_util`` here
 # to avoid having this code depend on the
 # of the Python build system.
+import io
 import os
 import pprint
 import logging
@@ -622,7 +623,7 @@ def mk_gparams_register_modules_internal(h_files_full_path, path):
     reg_mod_descr_pat = re.compile('[ \t]*REG_MODULE_DESCRIPTION\(\'([^\']*)\', *\'([^\']*)\'\)')
     for h_file in sorted_headers_by_component(h_files_full_path):
         added_include = False
-        with open(h_file, 'r') as fin:
+        with io.open(h_file, encoding='utf-8', mode='r') as fin:
             for line in fin:
                 m = reg_pat.match(line)
                 if m:
@@ -696,7 +697,7 @@ def mk_install_tactic_cpp_internal(h_files_full_path, path):
     for h_file in sorted_headers_by_component(h_files_full_path):
         added_include = False
         try:
-            with open(h_file, 'r') as fin:
+            with io.open(h_file, encoding='utf-8', mode='r') as fin:
                 for line in fin:
                     if tactic_pat.match(line):
                         if not added_include:
@@ -764,7 +765,7 @@ def mk_mem_initializer_cpp_internal(h_files_full_path, path):
     finalizer_pat        = re.compile('[ \t]*ADD_FINALIZER\(\'([^\']*)\'\)')
     for h_file in sorted_headers_by_component(h_files_full_path):
         added_include = False
-        with open(h_file, 'r') as fin:
+        with io.open(h_file, encoding='utf-8', mode='r') as fin:
             for line in fin:
                 m = initializer_pat.match(line)
                 if m:
diff --git a/scripts/mk_nuget_release.py b/scripts/mk_nuget_release.py
index c5079ed2c..ba0d44c3e 100644
--- a/scripts/mk_nuget_release.py
+++ b/scripts/mk_nuget_release.py
@@ -38,7 +38,7 @@ def download_installs():
         urllib.request.urlretrieve(url, "packages/%s" % name)
 
 os_info = {"z64-ubuntu-14" : ('so', 'ubuntu.14.04-x64'),
-           'ubuntu-16' : ('so', 'ubuntu.16.04-x64'),
+           'ubuntu-16' : ('so', 'ubuntu-x64'),
            'x64-win' : ('dll', 'win-x64'),
            'x86-win' : ('dll', 'win-x86'),
            'osx' : ('dylib', 'macos'),
@@ -91,11 +91,7 @@ def create_nuget_spec():
         <iconUrl>https://raw.githubusercontent.com/Z3Prover/z3/master/package/icon.jpg</iconUrl>
         <projectUrl>https://github.com/Z3Prover/z3</projectUrl>
         <licenseUrl>https://raw.githubusercontent.com/Z3Prover/z3/master/LICENSE.txt</licenseUrl>
-        <repository
-            type="git"
-            url="https://github.com/Z3Prover/z3.git"
-            branch="master"
-        />
+        <repository type="git" url="https://github.com/Z3Prover/z3.git" />
         <requireLicenseAcceptance>true</requireLicenseAcceptance>
         <language>en</language>
     </metadata>
diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 9076b582f..6552a942f 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -6,6 +6,7 @@
 #
 # Author: Leonardo de Moura (leonardo)
 ############################################
+import io
 import sys
 import os
 import re
@@ -806,7 +807,7 @@ def extract_c_includes(fname):
     # We should generate and error for any occurrence of #include that does not match the previous pattern.
     non_std_inc_pat = re.compile(".*#include.*")
 
-    f = open(fname, 'r')
+    f = io.open(fname, encoding='utf-8', mode='r')
     linenum = 1
     for line in f:
         m1 = std_inc_pat.match(line)
diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp
index a5ad7b525..8f92d5bb4 100644
--- a/src/api/api_solver.cpp
+++ b/src/api/api_solver.cpp
@@ -181,7 +181,7 @@ extern "C" {
         if (!is) {
             SET_ERROR_CODE(Z3_FILE_ACCESS_ERROR, nullptr);
         }
-        else if (ext && std::string("dimacs") == ext) {
+        else if (ext && (std::string("dimacs") == ext || std::string("cnf") == ext)) {
             ast_manager& m = to_solver_ref(s)->get_manager();
             std::stringstream err;
             sat::solver solver(to_solver_ref(s)->get_params(), m.limit());
diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index 7d45c9707..e541080c9 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -1720,6 +1720,10 @@ namespace z3 {
             m_vector = s.m_vector;
             return *this;
         }
+        ast_vector_tpl& set(unsigned idx, ast& a) {
+            Z3_ast_vector_set(ctx(), m_vector, idx, a);
+            return *this;
+        }
         /*
           Disabled pending C++98 build upgrade
         bool contains(T const& x) const {
@@ -1746,6 +1750,9 @@ namespace z3 {
                 ++m_index;
                 return *this;
             }
+            void set(T& arg) {
+                Z3_ast_vector_set(m_vector->ctx(), *m_vector, m_index, arg);
+            }
             iterator operator++(int) { iterator tmp = *this; ++m_index; return tmp; }
             T * operator->() const { return &(operator*()); }
             T operator*() const { return (*m_vector)[m_index]; }
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..5e528f15e 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 {
@@ -584,13 +654,14 @@ namespace datatype {
             param_size::size* sz;
             obj_map<sort, param_size::size*> S;
             unsigned n = get_datatype_num_parameter_sorts(s);
+            def & d = get_def(s->get_name());
+            SASSERT(n == d.params().size());
             for (unsigned i = 0; i < n; ++i) {
                 sort* ps = get_datatype_parameter_sort(s, i);
                 sz = get_sort_size(params, ps);
-                sz->inc_ref();
-                S.insert(ps, sz); 
-            }
-            def & d = get_def(s->get_name());
+                sz->inc_ref();                
+                S.insert(d.params().get(i), sz); 
+            }            
             sz = d.sort_size()->subst(S);
             for (auto & kv : S) {
                 kv.m_value->dec_ref();
@@ -667,7 +738,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/ast/expr2var.cpp b/src/ast/expr2var.cpp
index b1fdba2b5..61adcfc3a 100644
--- a/src/ast/expr2var.cpp
+++ b/src/ast/expr2var.cpp
@@ -29,8 +29,17 @@ void expr2var::insert(expr * n, var v) {
         TRACE("expr2var", tout << "interpreted:\n" << mk_ismt2_pp(n, m()) << "\n";);
         m_interpreted_vars = true;
     }
-    m().inc_ref(n);
-    m_mapping.insert(n, v);
+    unsigned idx = m_id2map.get(n->get_id(), UINT_MAX);
+    if (idx == UINT_MAX) {
+        m().inc_ref(n);
+        idx = m_mapping.size();
+        m_mapping.push_back(key_value(n, v));
+        m_id2map.setx(n->get_id(), idx, UINT_MAX);
+    }
+    else {
+        m_mapping[idx] = key_value(n, v);
+    }
+
     m_recent_exprs.push_back(n);
 }
 
@@ -40,20 +49,22 @@ expr2var::expr2var(ast_manager & m):
 }
 
 expr2var::~expr2var() {
-    dec_ref_map_keys(m(), m_mapping);
+    for (auto & kv : m_mapping) {
+        m().dec_ref(kv.m_key);
+    }
 }
 
 expr2var::var expr2var::to_var(expr * n) const {
-    var v = UINT_MAX;
-    m_mapping.find(n, v);
+    var v = m_id2map.get(n->get_id(), UINT_MAX);
+    if (v != UINT_MAX) {
+        v = m_mapping[v].m_value;
+    }
     return v;
 }
 
 void expr2var::display(std::ostream & out) const {
-    obj_map<expr, var>::iterator it  = m_mapping.begin();
-    obj_map<expr, var>::iterator end = m_mapping.end();
-    for (; it != end; ++it) {
-        out << mk_ismt2_pp(it->m_key, m()) << " -> " << it->m_value << "\n";
+    for (auto const& kv : m_mapping) {
+        out << mk_ismt2_pp(kv.m_key, m()) << " -> " << kv.m_value << "\n";
     }
 }
 
@@ -68,8 +79,11 @@ void expr2var::mk_inv(expr_ref_vector & var2expr) const {
 }
 
 void expr2var::reset() {
-    dec_ref_map_keys(m(), m_mapping);
-    SASSERT(m_mapping.empty());
+    for (auto & kv : m_mapping) {
+        m().dec_ref(kv.m_key);
+    }
+    m_mapping.reset();
+    m_id2map.reset();
     m_recent_exprs.reset();
     m_recent_lim.reset();
     m_interpreted_vars = false;
@@ -83,8 +97,15 @@ void expr2var::pop(unsigned num_scopes) {
     if (num_scopes > 0) {
         unsigned sz = m_recent_lim[m_recent_lim.size() - num_scopes];
         for (unsigned i = sz; i < m_recent_exprs.size(); ++i) {
-            m_mapping.erase(m_recent_exprs[i]);
-            m().dec_ref(m_recent_exprs[i]);
+            expr* n = m_recent_exprs[i];
+            unsigned idx = m_id2map[n->get_id()];
+            if (idx + 1 != m_mapping.size()) {
+                m_id2map[m_mapping.back().m_key->get_id()] = idx;
+                m_mapping[idx] = m_mapping.back();
+            }
+            m_id2map[n->get_id()] = UINT_MAX;
+            m_mapping.pop_back();
+            m().dec_ref(n);
         }
         m_recent_exprs.shrink(sz);
         m_recent_lim.shrink(m_recent_lim.size() - num_scopes);
diff --git a/src/ast/expr2var.h b/src/ast/expr2var.h
index 2b4d8c3fe..2bf2fe160 100644
--- a/src/ast/expr2var.h
+++ b/src/ast/expr2var.h
@@ -32,12 +32,14 @@ Notes:
 class expr2var {
 public:
     typedef unsigned var;
-    typedef obj_map<expr, var> expr2var_mapping;
-    typedef expr2var_mapping::iterator iterator;
+    typedef obj_map<expr, var>::key_data key_value;
+    typedef key_value const* iterator;
     typedef ptr_vector<expr>::const_iterator recent_iterator;
 protected:
     ast_manager &    m_manager;
-    expr2var_mapping m_mapping;
+    
+    unsigned_vector    m_id2map;
+    svector<key_value> m_mapping;
     ptr_vector<expr> m_recent_exprs;
     unsigned_vector  m_recent_lim;
     bool             m_interpreted_vars;
@@ -51,7 +53,7 @@ public:
     
     var to_var(expr * n) const;
     
-    bool is_var(expr * n) const { return m_mapping.contains(n); }
+    bool is_var(expr * n) const { return m_id2map.get(n->get_id(), UINT_MAX) != UINT_MAX; }
 
     void display(std::ostream & out) const;
     
diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp
index 3dc76da5e..f6b760f9c 100644
--- a/src/ast/rewriter/bv_rewriter.cpp
+++ b/src/ast/rewriter/bv_rewriter.cpp
@@ -196,6 +196,9 @@ br_status bv_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * cons
         return mk_bv_comp(args[0], args[1], result);
     case OP_MKBV:
         return mk_mkbv(num_args, args, result);
+    case OP_BIT2BOOL:
+        SASSERT(num_args == 1);
+        return mk_bit2bool(args[0], f->get_parameter(0).get_int(), result);
     case OP_BSMUL_NO_OVFL:
         return mk_bvsmul_no_overflow(num_args, args, result);
     case OP_BUMUL_NO_OVFL:
@@ -2203,6 +2206,19 @@ br_status bv_rewriter::mk_bv_mul(unsigned num_args, expr * const * args, expr_re
     return st;
 }
 
+br_status bv_rewriter::mk_bit2bool(expr * n, int idx, expr_ref & result) {
+    rational v, bit;
+    unsigned sz = 0;
+    if (!is_numeral(n, v, sz)) 
+        return BR_FAILED;
+    if (idx < 0 || idx >= static_cast<int>(sz)) 
+        return BR_FAILED;
+    div(v, rational::power_of_two(idx), bit);
+    mod(bit, rational(2), bit);
+    result = m().mk_bool_val(bit.is_one());
+    return BR_DONE;
+}
+
 br_status bv_rewriter::mk_bit2bool(expr * lhs, expr * rhs, expr_ref & result) {
     unsigned sz = get_bv_size(lhs);
     if (sz != 1)
diff --git a/src/ast/rewriter/bv_rewriter.h b/src/ast/rewriter/bv_rewriter.h
index 205ebbf8e..8ad589a49 100644
--- a/src/ast/rewriter/bv_rewriter.h
+++ b/src/ast/rewriter/bv_rewriter.h
@@ -134,6 +134,7 @@ class bv_rewriter : public poly_rewriter<bv_rewriter_core> {
     br_status mk_bv_redand(expr * arg, expr_ref & result);
     br_status mk_bv_comp(expr * arg1, expr * arg2, expr_ref & result);
     br_status mk_bit2bool(expr * lhs, expr * rhs, expr_ref & result);
+    br_status mk_bit2bool(expr * lhs, int idx, expr_ref & result);
     br_status mk_blast_eq_value(expr * lhs, expr * rhs, expr_ref & result);
     br_status mk_eq_concat(expr * lhs, expr * rhs, expr_ref & result);
     br_status mk_mkbv(unsigned num, expr * const * args, expr_ref & result);
diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index d46f234e2..cb915d86b 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -459,6 +459,11 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
     case OP_SEQ_AT:
         SASSERT(num_args == 2);
         return mk_seq_at(args[0], args[1], result); 
+#if 0
+    case OP_SEQ_NTH:
+        SASSERT(num_args == 2);
+        return mk_seq_nth(args[0], args[1], result); 
+#endif
     case OP_SEQ_PREFIX: 
         SASSERT(num_args == 2);
         return mk_seq_prefix(args[0], args[1], result);
@@ -877,6 +882,32 @@ br_status seq_rewriter::mk_seq_at(expr* a, expr* b, expr_ref& result) {
     return BR_DONE;
 }
 
+br_status seq_rewriter::mk_seq_nth(expr* a, expr* b, expr_ref& result) {
+    zstring c;
+    rational r;
+    if (!m_autil.is_numeral(b, r) || !r.is_unsigned()) {
+        return BR_FAILED;
+    }
+    unsigned len = r.get_unsigned();
+
+    expr_ref_vector as(m());
+    m_util.str.get_concat_units(a, as);
+
+    for (unsigned i = 0; i < as.size(); ++i) {
+        expr* a = as.get(i), *u = nullptr;
+        if (m_util.str.is_unit(a, u)) {
+            if (len == i) {
+                result = u;
+                return BR_DONE;
+            }            
+        }
+        else {
+            return BR_FAILED;
+        }
+    }
+    return BR_FAILED;
+}
+
 br_status seq_rewriter::mk_seq_index(expr* a, expr* b, expr* c, expr_ref& result) {
     zstring s1, s2;
     rational r;
diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h
index 83793a594..25b8979fc 100644
--- a/src/ast/rewriter/seq_rewriter.h
+++ b/src/ast/rewriter/seq_rewriter.h
@@ -114,6 +114,7 @@ class seq_rewriter {
     br_status mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& result);
     br_status mk_seq_contains(expr* a, expr* b, expr_ref& result);
     br_status mk_seq_at(expr* a, expr* b, expr_ref& result);
+    br_status mk_seq_nth(expr* a, expr* b, expr_ref& result);
     br_status mk_seq_index(expr* a, expr* b, expr* c, expr_ref& result);
     br_status mk_seq_replace(expr* a, expr* b, expr* c, expr_ref& result);
     br_status mk_seq_prefix(expr* a, expr* b, expr_ref& result);
diff --git a/src/ast/shared_occs.cpp b/src/ast/shared_occs.cpp
index 89867e8c1..9528892e7 100644
--- a/src/ast/shared_occs.cpp
+++ b/src/ast/shared_occs.cpp
@@ -21,13 +21,11 @@ Revision History:
 #include "util/ref_util.h"
 
 inline void shared_occs::insert(expr * t) {
-    obj_hashtable<expr>::entry * dummy;
-    if (m_shared.insert_if_not_there_core(t, dummy))
-        m.inc_ref(t);
+    m_shared.reserve(t->get_id() + 1);
+    m_shared[t->get_id()] = t;
 }
 
 void shared_occs::reset() { 
-    dec_ref_collection_values(m, m_shared);
     m_shared.reset(); 
 }
 
@@ -132,9 +130,15 @@ void shared_occs::operator()(expr * t) {
 }
 
 void shared_occs::display(std::ostream & out, ast_manager & m) const {
-    iterator it =  begin_shared();
-    iterator end = end_shared();
-    for (; it != end; ++it) {
-        out << mk_ismt2_pp(*it, m) << "\n";
+    for (expr* s : m_shared) {
+        if (s) {
+            out << mk_ismt2_pp(s, m) << "\n";
+        }
     }
 }
+
+unsigned shared_occs::num_shared() const{ 
+    unsigned count = 0;
+    for (expr* s : m_shared) if (s) count++;
+    return count;
+}
diff --git a/src/ast/shared_occs.h b/src/ast/shared_occs.h
index 40921922a..300bb584f 100644
--- a/src/ast/shared_occs.h
+++ b/src/ast/shared_occs.h
@@ -53,7 +53,7 @@ class shared_occs {
     bool                m_track_atomic;
     bool                m_visit_quantifiers;
     bool                m_visit_patterns;
-    obj_hashtable<expr> m_shared;
+    expr_ref_vector     m_shared;
     typedef std::pair<expr*, unsigned> frame;
     svector<frame>      m_stack;
     bool process(expr * t, shared_occs_mark & visited);
@@ -64,15 +64,14 @@ public:
         m(_m),
         m_track_atomic(track_atomic),
         m_visit_quantifiers(visit_quantifiers),
-        m_visit_patterns(visit_patterns) {
+        m_visit_patterns(visit_patterns),
+        m_shared(m) {
     }
     ~shared_occs();
     void operator()(expr * t);
     void operator()(expr * t, shared_occs_mark & visited);
-    bool is_shared(expr * t) const { return m_shared.contains(t); }
-    unsigned num_shared() const { return m_shared.size(); }
-    iterator begin_shared() const { return m_shared.begin(); }
-    iterator end_shared() const { return m_shared.end(); }
+    bool is_shared(expr * t) const { return m_shared.get(t->get_id(), nullptr) != nullptr; }
+    unsigned num_shared() const;
     void reset();
     void cleanup();
     void display(std::ostream & out, ast_manager & mgr) const;
diff --git a/src/cmd_context/extra_cmds/dbg_cmds.cpp b/src/cmd_context/extra_cmds/dbg_cmds.cpp
index bdd2c8b97..7c1383d62 100644
--- a/src/cmd_context/extra_cmds/dbg_cmds.cpp
+++ b/src/cmd_context/extra_cmds/dbg_cmds.cpp
@@ -77,30 +77,12 @@ BINARY_SYM_CMD(shift_vars_cmd,
     store_expr_ref(ctx, m_sym, r.get());
 });
 
-UNARY_CMD(pp_shared_cmd, "dbg-pp-shared", "<term>", "display shared subterms of the given term", CPK_EXPR, expr *, {
-    shared_occs s(ctx.m());
-    s(arg);
-    ctx.regular_stream() << "(shared";
-    shared_occs::iterator it  = s.begin_shared();
-    shared_occs::iterator end = s.end_shared();
-    for (; it != end; ++it) {
-        expr * curr = *it;
-        ctx.regular_stream() << std::endl << "  ";
-        ctx.display(ctx.regular_stream(), curr, 2);
-    }
-    ctx.regular_stream() << ")" << std::endl;
-});
 
 UNARY_CMD(assert_not_cmd, "assert-not", "<term>", "assert negation", CPK_EXPR, expr *, {
     expr_ref ne(ctx.m().mk_not(arg), ctx.m());
     ctx.assert_expr(ne);
 });
 
-UNARY_CMD(num_shared_cmd, "dbg-num-shared", "<term>", "return the number of shared subterms", CPK_EXPR, expr *, {
-    shared_occs s(ctx.m());
-    s(arg);
-    ctx.regular_stream() << s.num_shared() << std::endl;
-});
 
 UNARY_CMD(size_cmd, "dbg-size", "<term>", "return the size of the given term", CPK_EXPR, expr *, {
     ctx.regular_stream() << get_num_exprs(arg) << std::endl;
@@ -524,11 +506,21 @@ public:
         for (func_decl* v : m_vars) vars.push_back(v);
         for (expr* e : m_lits) lits.push_back(e);
         flatten_and(lits);
-        qe::term_graph tg(m);
-        tg.set_vars(vars, false);
-        tg.add_lits(lits);
-        expr_ref_vector p = tg.project();
-        ctx.regular_stream() << p << "\n";
+        solver_factory& sf = ctx.get_solver_factory();
+        params_ref pa;
+        solver_ref s = sf(m, pa, false, true, true, symbol::null);
+        solver_ref se = sf(m, pa, false, true, true, symbol::null);
+        s->assert_expr(lits);
+        lbool r = s->check_sat();
+        if (r != l_true) {
+            ctx.regular_stream() << "sat check " << r << "\n";
+            return;
+        }
+        model_ref mdl;
+        s->get_model(mdl);
+        qe::euf_arith_mbi_plugin plugin(s.get(), se.get());
+        plugin.project(mdl, lits);
+        ctx.regular_stream() << lits << "\n";
     }
 
 };
@@ -540,8 +532,6 @@ void install_dbg_cmds(cmd_context & ctx) {
     ctx.insert(alloc(set_cmd));
     ctx.insert(alloc(pp_var_cmd));
     ctx.insert(alloc(shift_vars_cmd));
-    ctx.insert(alloc(pp_shared_cmd));
-    ctx.insert(alloc(num_shared_cmd));
     ctx.insert(alloc(assert_not_cmd));
     ctx.insert(alloc(size_cmd));
     ctx.insert(alloc(subst_cmd));
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 66c175ac8..d23fd5043 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -361,7 +361,7 @@ namespace opt {
         mdl = m_model;
         fix_model(mdl);
         if (mdl) mdl->set_model_completion(true);
-        TRACE("opt", tout << *mdl;);
+        CTRACE("opt", mdl, tout << *mdl;);
     }
 
     void context::get_box_model(model_ref& mdl, unsigned index) {
diff --git a/src/qe/qe_arrays.cpp b/src/qe/qe_arrays.cpp
index 4c81418b6..4bead6684 100644
--- a/src/qe/qe_arrays.cpp
+++ b/src/qe/qe_arrays.cpp
@@ -798,7 +798,7 @@ namespace qe {
          */
         expr* reduce_core (app *a) {
             if (!m_arr_u.is_store (a->get_arg (0))) return a;
-			expr* array = a->get_arg(0);
+            expr* array = a->get_arg(0);
             unsigned arity = get_array_arity(m.get_sort(array));
 
             expr* const* js = a->get_args() + 1;
@@ -810,7 +810,7 @@ namespace qe {
 
                 if (is_equals (arity, idxs, js)) {
                     add_idx_cond (cond);
-                    return a->get_arg (2);
+                    return a->get_arg (a->get_num_args() - 1);
                 }
                 else {
                     cond = m.mk_not (cond);
diff --git a/src/qe/qe_mbi.cpp b/src/qe/qe_mbi.cpp
index b7de8d302..77f910260 100644
--- a/src/qe/qe_mbi.cpp
+++ b/src/qe/qe_mbi.cpp
@@ -126,30 +126,29 @@ namespace qe {
     struct euf_arith_mbi_plugin::is_arith_var_proc {
         ast_manager&    m;
         app_ref_vector& m_avars;
-        arith_util      arith;
+        app_ref_vector& m_proxies;
+        arith_util      m_arith;
         obj_hashtable<expr> m_seen;
-        is_arith_var_proc(app_ref_vector& avars):
-            m(avars.m()), m_avars(avars), arith(m) {
+        is_arith_var_proc(app_ref_vector& avars, app_ref_vector& proxies):
+            m(avars.m()), m_avars(avars), m_proxies(proxies), m_arith(m) {
         }
         void operator()(app* a) {
             if (is_arith_op(a) || a->get_family_id() == m.get_basic_family_id()) {
-                // no-op
+                return;
             }
-            else if (!arith.is_int_real(a)) {
-                for (expr* arg : *a) {
-                    if (is_app(arg) && !m_seen.contains(arg) && is_arith_op(to_app(arg))) {
-                        m_avars.push_back(to_app(arg));
-                        m_seen.insert(arg);
-                    }
-                }
-            }
-            else if (!m_seen.contains(a)) {
-                m_seen.insert(a);
+
+            if (m_arith.is_int_real(a)) {
                 m_avars.push_back(a);
             }
+            for (expr* arg : *a) {
+                if (is_app(arg) && !m_seen.contains(arg) && m_arith.is_int_real(arg)) {
+                    m_proxies.push_back(to_app(arg));
+                    m_seen.insert(arg);
+                }
+            }
         }
         bool is_arith_op(app* a) {
-            return a->get_family_id() == arith.get_family_id();
+            return a->get_family_id() == m_arith.get_family_id();
         }
         void operator()(expr*) {}
     };
@@ -221,9 +220,9 @@ namespace qe {
     /** 
      * \brief extract arithmetical variables and arithmetical terms in shared positions.
      */
-    app_ref_vector euf_arith_mbi_plugin::get_arith_vars(model_ref& mdl, expr_ref_vector& lits) {
+    app_ref_vector euf_arith_mbi_plugin::get_arith_vars(model_ref& mdl, expr_ref_vector& lits, app_ref_vector& proxies) {
         app_ref_vector avars(m); 
-        is_arith_var_proc _proc(avars);
+        is_arith_var_proc _proc(avars, proxies);
         for_each_expr(_proc, lits);
         return avars;
     }
@@ -257,16 +256,19 @@ namespace qe {
 
     void euf_arith_mbi_plugin::project(model_ref& mdl, expr_ref_vector& lits) {
         TRACE("qe", tout << lits << "\n" << *mdl << "\n";);
+        TRACE("qe", tout << m_solver->get_assertions() << "\n";);
+
 
         // 1. arithmetical variables - atomic and in purified positions
-        app_ref_vector avars = get_arith_vars(mdl, lits);
-        TRACE("qe", tout << "vars: " << avars << "\nlits: " << lits << "\n";);
+        app_ref_vector proxies(m);
+        app_ref_vector avars = get_arith_vars(mdl, lits, proxies);
+        TRACE("qe", tout << "vars: " << avars << "\nproxies: " << proxies << "\nlits: " << lits << "\n";);
 
         // 2. project private non-arithmetical variables from lits
         project_euf(mdl, lits, avars);
 
         // 3. Order arithmetical variables and purified positions
-        order_avars(mdl, lits, avars);
+        order_avars(mdl, lits, avars, proxies);
         TRACE("qe", tout << "ordered: " << lits << "\n";);
 
         // 4. Perform arithmetical projection
@@ -307,15 +309,14 @@ namespace qe {
 
     /**
      * \brief Order arithmetical variables:
-     * 1. add literals that order the variable according to the model.
-     * 2. remove non-atomic arithmetical terms from projection.
+     * 1. add literals that order the proxies according to the model.
      * 2. sort arithmetical terms, such that deepest terms are first.
      */
-    void euf_arith_mbi_plugin::order_avars(model_ref& mdl, expr_ref_vector& lits, app_ref_vector& avars) {
+    void euf_arith_mbi_plugin::order_avars(model_ref& mdl, expr_ref_vector& lits, app_ref_vector& avars, app_ref_vector const& proxies) {
         arith_util a(m);
         model_evaluator mev(*mdl.get());
         vector<std::pair<rational, app*>> vals;
-        for (app* v : avars) {
+        for (app* v : proxies) {
             rational val;
             expr_ref tmp = mev(v);
             VERIFY(a.is_numeral(tmp, val));
@@ -327,7 +328,7 @@ namespace qe {
                 return x.first < y.first;
             }
         };
-        // add linear order between avars
+        // add linear order between proxies
         compare_first cmp;
         std::sort(vals.begin(), vals.end(), cmp);
         for (unsigned i = 1; i < vals.size(); ++i) {
@@ -338,6 +339,7 @@ namespace qe {
                 lits.push_back(a.mk_lt(vals[i-1].second, vals[i].second));
             }
         }
+
         // filter out only private variables
         filter_private_arith(avars);
 
diff --git a/src/qe/qe_mbi.h b/src/qe/qe_mbi.h
index 23294ee6e..12e6a8080 100644
--- a/src/qe/qe_mbi.h
+++ b/src/qe/qe_mbi.h
@@ -103,18 +103,18 @@ namespace qe {
         struct is_atom_proc;
         struct is_arith_var_proc;
 
-        app_ref_vector get_arith_vars(model_ref& mdl, expr_ref_vector& lits);
+        app_ref_vector get_arith_vars(model_ref& mdl, expr_ref_vector& lits, app_ref_vector& proxies);
         bool get_literals(model_ref& mdl, expr_ref_vector& lits);
         void collect_atoms(expr_ref_vector const& fmls);
-        void project(model_ref& mdl, expr_ref_vector& lits);
         void project_euf(model_ref& mdl, expr_ref_vector& lits, app_ref_vector& avars);
-        void order_avars(model_ref& mdl, expr_ref_vector& lits, app_ref_vector& avars);
+        void order_avars(model_ref& mdl, expr_ref_vector& lits, app_ref_vector& avars, app_ref_vector const& proxies);
         void substitute(vector<def> const& defs, expr_ref_vector& lits);
         void filter_private_arith(app_ref_vector& avars);
     public:
         euf_arith_mbi_plugin(solver* s, solver* emptySolver);
         ~euf_arith_mbi_plugin() override {}
         mbi_result operator()(expr_ref_vector& lits, model_ref& mdl) override;
+        void project(model_ref& mdl, expr_ref_vector& lits);
         void block(expr_ref_vector const& lits) override;
     };
 
diff --git a/src/qe/qe_mbp.cpp b/src/qe/qe_mbp.cpp
index a0e16727e..becaeb049 100644
--- a/src/qe/qe_mbp.cpp
+++ b/src/qe/qe_mbp.cpp
@@ -501,7 +501,7 @@ public:
         expr_ref val(m);
         model_evaluator eval(model);
         for (expr * f : fmls) {
-            VERIFY(model.is_true(f));
+            VERIFY(!model.is_false(f));
         }
         return true;
     }
@@ -657,7 +657,7 @@ public:
             other_vars.reset();
         }
         
-        SASSERT(eval.is_true(fml));
+        SASSERT(!eval.is_false(fml));
                 
         vars.reset ();
         vars.append(other_vars);
diff --git a/src/sat/sat_cleaner.cpp b/src/sat/sat_cleaner.cpp
index c0c6fabe4..4a3fb82b4 100644
--- a/src/sat/sat_cleaner.cpp
+++ b/src/sat/sat_cleaner.cpp
@@ -78,6 +78,7 @@ namespace sat {
     }
 
     void cleaner::cleanup_clauses(clause_vector & cs) {
+        tmp_clause tmp;
         clause_vector::iterator it  = cs.begin();
         clause_vector::iterator it2 = it;
         clause_vector::iterator end = cs.end();
@@ -88,12 +89,10 @@ namespace sat {
             CTRACE("sat_cleaner_frozen", c.frozen(), tout << c << "\n";);
             unsigned sz = c.size();
             unsigned i = 0, j = 0;
-            bool sat = false;
             m_cleanup_counter += sz;
             for (; i < sz; i++) {
                 switch (s.value(c[i])) {
                 case l_true:
-                    sat = true;
                     goto end_loop;
                 case l_false:
                     m_elim_literals++;
@@ -108,9 +107,9 @@ namespace sat {
             }
         end_loop:
             CTRACE("sat_cleaner_frozen", c.frozen(),
-                   tout << "sat: " << sat << ", new_size: " << j << "\n";
+                   tout << "sat: " << (i < sz) << ", new_size: " << j << "\n";
                    tout << mk_lits_pp(j, c.begin()) << "\n";);
-            if (sat) {
+            if (i < sz) {
                 m_elim_clauses++;
                 s.del_clause(c);
             }
@@ -119,33 +118,37 @@ namespace sat {
                 CTRACE("sat_cleaner_bug", new_sz < 2, tout << "new_sz: " << new_sz << "\n";
                        if (c.size() > 0) tout << "unit: " << c[0] << "\n";
                        s.display_watches(tout););
-                if (new_sz == 0) {
+                switch (new_sz) {
+                case 0:
                     s.set_conflict(justification());
                     s.del_clause(c);
-                }
-                else if (new_sz == 1) {
+                    break;
+                case 1:
                     s.assign(c[0], justification());
                     s.del_clause(c);
-                }
-                else {
+                    break;
+                case 2:
                     SASSERT(s.value(c[0]) == l_undef && s.value(c[1]) == l_undef);
-                    if (new_sz == 2) {
-                        TRACE("cleanup_bug", tout << "clause became binary: " << c[0] << " " << c[1] << "\n";);
-                        s.mk_bin_clause(c[0], c[1], c.is_learned());
-                        s.del_clause(c);
+                    TRACE("cleanup_bug", tout << "clause became binary: " << c[0] << " " << c[1] << "\n";);
+                    s.mk_bin_clause(c[0], c[1], c.is_learned());
+                    s.del_clause(c);
+                    break;
+                default:
+                    SASSERT(s.value(c[0]) == l_undef && s.value(c[1]) == l_undef);
+                    if (s.m_config.m_drat && new_sz < i) {
+                        tmp.set(c.size(), c.begin(), c.is_learned());
                     }
-                    else {
-                        c.shrink(new_sz);
-                        *it2 = *it;
-                        it2++;
-                        if (!c.frozen()) {                            
-                            s.attach_clause(c);
-                        }
-                        if (s.m_config.m_drat) {
-                            // for optimization, could also report deletion 
-                            // of previous version of clause.
-                            s.m_drat.add(c, true);
-                        }
+                    c.shrink(new_sz);
+                    *it2 = *it;
+                    it2++;
+                    if (!c.frozen()) {                            
+                        s.attach_clause(c);
+                    }
+                    if (s.m_config.m_drat && new_sz < i) {
+                        // for optimization, could also report deletion 
+                        // of previous version of clause.
+                        s.m_drat.add(c, true);
+                        s.m_drat.del(*tmp.get());
                     }
                 }
             }
@@ -192,10 +195,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;
     }
diff --git a/src/sat/sat_drat.cpp b/src/sat/sat_drat.cpp
index 529a6bc57..4707fa0ac 100644
--- a/src/sat/sat_drat.cpp
+++ b/src/sat/sat_drat.cpp
@@ -143,7 +143,7 @@ namespace sat {
         IF_VERBOSE(20, trace(verbose_stream(), n, c.begin(), st););
 
         if (st == status::learned) {
-            verify(n, c.begin());
+            verify(c);
         }
 
         m_status.push_back(st);
@@ -225,6 +225,55 @@ namespace sat {
         m_units.resize(num_units);
         bool ok = m_inconsistent;
         m_inconsistent = false;
+
+        if (!ok) {
+            literal_vector lits(n, c);
+            IF_VERBOSE(0, verbose_stream() << "not drup " << lits << "\n");
+            for (unsigned v = 0; v < m_assignment.size(); ++v) {
+                lbool val = m_assignment[v];
+                if (val != l_undef) {
+                    IF_VERBOSE(0, verbose_stream() << literal(v, false) << " |-> " << val << "\n");
+                }
+            }
+            for (clause* cp : s.m_clauses) {
+                clause& cl = *cp;
+                bool found = false;
+                for (literal l : cl) {
+                    if (m_assignment[l.var()] != (l.sign() ? l_true : l_false)) {
+                        found = true;
+                        break;
+                    }
+                }
+                if (!found) {
+                    IF_VERBOSE(0, verbose_stream() << "Clause is false under assignment: " << cl << "\n");
+                }
+            }
+            for (clause* cp : s.m_learned) {
+                clause& cl = *cp;
+                bool found = false;
+                for (literal l : cl) {
+                    if (m_assignment[l.var()] != (l.sign() ? l_true : l_false)) {
+                        found = true;
+                        break;
+                    }
+                }
+                if (!found) {
+                    IF_VERBOSE(0, verbose_stream() << "Clause is false under assignment: " << cl << "\n");
+                }
+            }
+            svector<sat::solver::bin_clause> bin;
+            s.collect_bin_clauses(bin, true);
+            for (auto & b : bin) {
+                bool found = false;
+                if (m_assignment[b.first.var()] != (b.first.sign() ? l_true : l_false)) found = true;
+                if (m_assignment[b.second.var()] != (b.second.sign() ? l_true : l_false)) found = true;
+                if (!found) {
+                    IF_VERBOSE(0, verbose_stream() << "Bin clause is false under assignment: " << b.first << " " << b.second << "\n");
+                }
+            }
+            IF_VERBOSE(0, s.display(verbose_stream()));
+            exit(0);
+        }
         return ok;
     }
 
@@ -280,7 +329,10 @@ namespace sat {
 
     void drat::verify(unsigned n, literal const* c) {
         if (m_check_unsat && !is_drup(n, c) && !is_drat(n, c)) {
-            std::cout << "Verification failed\n";
+            literal_vector lits(n, c);
+            std::cout << "Verification of " << lits << " failed\n";
+            s.display(std::cout);
+            exit(0);
             UNREACHABLE();
             //display(std::cout);
             TRACE("sat", 
@@ -291,6 +343,35 @@ namespace sat {
         }
     }
 
+    bool drat::contains(unsigned n, literal const* lits) {
+        for (unsigned i = m_proof.size(); i-- > 0; ) {
+            clause& c = *m_proof[i];
+            status st = m_status[i];
+            if (match(n, lits, c)) {
+                return st != status::deleted;
+            }
+        }
+        return false;
+    }
+
+    bool drat::match(unsigned n, literal const* lits, clause const& c) const {
+        if (n == c.size()) {
+            for (unsigned i = 0; i < n; ++i) {
+                literal lit1 = lits[i];
+                bool found = false;
+                for (literal lit2 : c) {
+                    if (lit1 == lit2) {
+                        found = true;
+                        break;
+                    }
+                }
+                if (!found) return false;
+            }
+            return true;
+        }
+        return false;
+    }
+
     void drat::display(std::ostream& out) const {
         out << "units: " << m_units << "\n";
         for (unsigned i = 0; i < m_assignment.size(); ++i) {
diff --git a/src/sat/sat_drat.h b/src/sat/sat_drat.h
index 64d796839..35da0c31a 100644
--- a/src/sat/sat_drat.h
+++ b/src/sat/sat_drat.h
@@ -67,7 +67,6 @@ namespace sat {
         void propagate(literal l);
         void assign_propagate(literal l);
         void del_watch(clause& c, literal l);
-        void verify(unsigned n, literal const* c);
         bool is_drup(unsigned n, literal const* c);
         bool is_drat(unsigned n, literal const* c);
         bool is_drat(unsigned n, literal const* c, unsigned pos);
@@ -75,6 +74,7 @@ namespace sat {
         void trace(std::ostream& out, unsigned n, literal const* c, status st);
         void display(std::ostream& out) const;
         void validate_propagation() const;
+        bool match(unsigned n, literal const* lits, clause const& c) const;
 
     public:
         drat(solver& s);
@@ -93,6 +93,16 @@ namespace sat {
         void del(literal l1, literal l2);
         void del(clause& c);
 
+        void verify(clause const& c) { verify(c.size(), c.begin()); }
+        void verify(unsigned n, literal const* c);
+        void verify(literal l1, literal l2) { literal lits[2] = {l1, l2}; verify(2, lits); }
+        void verify(literal l1, literal l2, literal l3) { literal lits[3] = {l1, l2, l3}; verify(3, lits); }
+
+        bool contains(clause const& c) { return contains(c.size(), c.begin()); }
+        bool contains(unsigned n, literal const* c);
+        bool contains(literal l1, literal l2) { literal lits[2] = {l1, l2}; return contains(2, lits); }
+        bool contains(literal l1, literal l2, literal l3) { literal lits[3] = {l1, l2, l3}; return contains(3, lits); }
+
         void check_model(model const& m);
     };
 
diff --git a/src/sat/sat_elim_eqs.cpp b/src/sat/sat_elim_eqs.cpp
index 870aa7fe2..8633f04d3 100644
--- a/src/sat/sat_elim_eqs.cpp
+++ b/src/sat/sat_elim_eqs.cpp
@@ -23,9 +23,15 @@ Revision History:
 namespace sat {
     
     elim_eqs::elim_eqs(solver & s):
-        m_solver(s) {
+        m_solver(s),
+        m_to_delete(nullptr) {
     }
 
+    elim_eqs::~elim_eqs() {
+        dealloc(m_to_delete);
+    }
+
+
     inline literal norm(literal_vector const & roots, literal l) {
         if (l.sign()) 
             return ~roots[l.var()];
@@ -86,6 +92,12 @@ namespace sat {
         m_new_bin.reset();
     }
 
+    void elim_eqs::drat_delete_clause() {
+        if (m_solver.m_config.m_drat) {
+            m_solver.m_drat.del(*m_to_delete->get()); 
+        }
+    }
+
     void elim_eqs::cleanup_clauses(literal_vector const & roots, clause_vector & cs) {
         clause_vector::iterator it  = cs.begin();
         clause_vector::iterator it2 = it;
@@ -107,8 +119,16 @@ namespace sat {
                 it2++;
                 continue;
             }
-            if (!c.frozen())
+            if (!c.frozen()) {
                 m_solver.detach_clause(c);
+            }
+            
+            // save clause to be deleted for drat
+            if (m_solver.m_config.m_drat) {
+                if (!m_to_delete) m_to_delete = alloc(tmp_clause);
+                m_to_delete->set(sz, c.begin(), c.is_learned());
+            }
+
             // apply substitution
             for (i = 0; i < sz; i++) {   
                 literal lit = c[i];
@@ -124,60 +144,69 @@ namespace sat {
                         CTRACE("sat", l != norm(roots, l), tout << l << " " << norm(roots, l) << "\n"; tout.flush(););
                         SASSERT(l == norm(roots, l));
                     } });
+
             // remove duplicates, and check if it is a tautology
-            literal l_prev = null_literal;
             unsigned j = 0;
+            literal l_prev = null_literal;
             for (i = 0; i < sz; i++) {
                 literal l = c[i];
-                if (l == l_prev)
-                    continue;
-                if (l == ~l_prev)
+                if (l == ~l_prev) {
                     break;
+                }
+                if (l == l_prev) {
+                    continue;
+                }
+                SASSERT(l != ~l_prev);
                 l_prev = l;
                 lbool val = m_solver.value(l);
-                if (val == l_true)
-                    break; // clause was satisfied
-                if (val == l_false)
+                if (val == l_true) {
+                    break;
+                }
+                if (val == l_false) {
                     continue; // skip
+                }
                 c[j] = l;                
                 j++;
             }
+            TRACE("elim_eqs", tout << "after removing duplicates: " << c << " j: " << j << "\n";);
+
             if (i < sz) {
-                // clause is a tautology or was simplified to true
-                m_solver.del_clause(c);
+                drat_delete_clause();
+                m_solver.del_clause(c, false);
                 continue; 
             }
-            if (j == 0) {
-                // empty clause
+
+            switch (j) {
+            case 0:
                 m_solver.set_conflict(justification());
                 for (; it != end; ++it) {
                     *it2 = *it;
                     it2++;
                 }
                 cs.set_end(it2);
-                return;
-            }
-            TRACE("elim_eqs", tout << "after removing duplicates: " << c << " j: " << j << "\n";);
-
-            SASSERT(j >= 1);
-            switch (j) {
+                return;                
             case 1:
                 m_solver.assign(c[0], justification());
-                m_solver.del_clause(c);
+                m_solver.del_clause(c, false);
+                drat_delete_clause();
                 break;
             case 2:
                 m_solver.mk_bin_clause(c[0], c[1], c.is_learned());
-                m_solver.del_clause(c);
+                m_solver.del_clause(c, false);
+                drat_delete_clause();
                 break;
             default:
                 SASSERT(*it == &c);
                 if (j < sz) {
-                    if (m_solver.m_config.m_drat) m_solver.m_drat.del(c); 
                     c.shrink(j);
-                    if (m_solver.m_config.m_drat) m_solver.m_drat.add(c, true); 
                 }
-                else
+                else {
                     c.update_approx();
+                }
+                if (m_solver.m_config.m_drat) {
+                    m_solver.m_drat.add(c, true); 
+                    drat_delete_clause();
+                }
 
                 DEBUG_CODE(for (literal l : c) VERIFY(l == norm(roots, l)););
                 
diff --git a/src/sat/sat_elim_eqs.h b/src/sat/sat_elim_eqs.h
index 143fcbb3f..ac132b213 100644
--- a/src/sat/sat_elim_eqs.h
+++ b/src/sat/sat_elim_eqs.h
@@ -23,6 +23,7 @@ Revision History:
 
 namespace sat {
     class solver;
+    class tmp_clause;
     
     class elim_eqs {
         struct bin {
@@ -32,6 +33,8 @@ namespace sat {
         };
         svector<bin> m_new_bin;
         solver & m_solver;
+        tmp_clause* m_to_delete;
+        void drat_delete_clause();
         void save_elim(literal_vector const & roots, bool_var_vector const & to_elim);
         void cleanup_clauses(literal_vector const & roots, clause_vector & cs);
         void cleanup_bin_watches(literal_vector const & roots);
@@ -39,6 +42,7 @@ namespace sat {
         bool check_clause(clause const& c, literal_vector const& roots) const;
     public:
         elim_eqs(solver & s);
+        ~elim_eqs();
         void operator()(literal_vector const & roots, bool_var_vector const & to_elim);
     };
 
diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index 21d264af5..4feeb4b05 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/src/sat/sat_simplifier.cpp
@@ -349,7 +349,7 @@ namespace sat {
             }
             if (sz == 2) {
                 s.mk_bin_clause(c[0], c[1], c.is_learned());
-                s.del_clause(c);
+                s.del_clause(c, false);
                 continue;
             }
             *it2 = *it;
@@ -611,10 +611,15 @@ namespace sat {
                 break;
             }
         }
-        if (j < sz) {
-            if (s.m_config.m_drat) s.m_drat.del(c);
+        if (j < sz && !r) {
+            if (s.m_config.m_drat) {
+                m_dummy.set(c.size(), c.begin(), c.is_learned());
+            }
             c.shrink(j);
-            if (s.m_config.m_drat) s.m_drat.add(c, true);
+            if (s.m_config.m_drat) {
+                s.m_drat.add(c, true);
+                s.m_drat.del(*m_dummy.get());
+            }
         }
         return r;
     }
@@ -1272,7 +1277,8 @@ namespace sat {
          * unless C contains lit, and it is a tautology.
          */
         bool add_ala() {
-            for (; m_ala_qhead < m_covered_clause.size(); ++m_ala_qhead) {
+            unsigned init_size = m_covered_clause.size();
+            for (; m_ala_qhead < m_covered_clause.size() && m_ala_qhead < 5*init_size; ++m_ala_qhead) {
                 literal l = m_covered_clause[m_ala_qhead];                
                 for (watched & w : s.get_wlist(~l)) {
                     if (w.is_binary_non_learned_clause()) {
@@ -1282,7 +1288,6 @@ namespace sat {
                             return true;
                         }
                         if (!s.is_marked(~lit)) {
-                            // if (m_covered_clause[0].var() == 10219) IF_VERBOSE(0, verbose_stream() << "ala: " << l << " " << lit << "\n");
                             m_covered_clause.push_back(~lit);
                             m_covered_antecedent.push_back(clause_ante(l, false));
                             s.mark_visited(~lit);
@@ -1312,7 +1317,6 @@ namespace sat {
                     if (lit1 == null_literal) {
                         return true;
                     }
-                    // if (m_covered_clause[0].var() == 10219) IF_VERBOSE(0, verbose_stream() << "ala: " << c << " " << lit1 << "\n");
                     m_covered_clause.push_back(~lit1);
                     m_covered_antecedent.push_back(clause_ante(c));
                     s.mark_visited(~lit1);
@@ -1527,6 +1531,7 @@ namespace sat {
                     block_covered_binary(w, l, blocked, k);
                     break;
                 }
+                s.checkpoint();
             }
         }
 
@@ -1552,6 +1557,7 @@ namespace sat {
                     s.set_learned(c);
                     break;
                 }
+                s.checkpoint();
             }
         }
 
@@ -2019,8 +2025,7 @@ namespace sat {
             for (auto & c2 : m_neg_cls) {
                 m_new_cls.reset();
                 if (!resolve(c1, c2, pos_l, m_new_cls))
-                    continue;
-                if (false && v == 767) IF_VERBOSE(0, verbose_stream() << "elim: " << c1 << " +  " << c2 << " -> " << m_new_cls << "\n");
+                    continue;                
                 TRACE("resolution_new_cls", tout << c1 << "\n" << c2 << "\n-->\n" << m_new_cls << "\n";);
                 if (cleanup_clause(m_new_cls))
                     continue; // clause is already satisfied.
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index fc5fce252..6731adc92 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -298,14 +298,14 @@ namespace sat {
         mk_clause(3, ls, learned);
     }
 
-    void solver::del_clause(clause& c) {
+    void solver::del_clause(clause& c, bool enable_drat) {
         if (!c.is_learned()) {
             m_stats.m_non_learned_generation++;
         } 
         if (c.frozen()) {
             --m_num_frozen;
         }
-        if (m_config.m_drat && !m_drat.is_cleaned(c)) {
+        if (enable_drat && m_config.m_drat && !m_drat.is_cleaned(c)) {
             m_drat.del(c);
         }
         dealloc_clause(&c);        
diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h
index 8402fc898..3937c67e8 100644
--- a/src/sat/sat_solver.h
+++ b/src/sat/sat_solver.h
@@ -232,7 +232,7 @@ namespace sat {
         void defrag_clauses();
         bool should_defrag();
         bool memory_pressure();
-        void del_clause(clause & c);
+        void del_clause(clause & c, bool enable_drat = true);
         clause * mk_clause_core(unsigned num_lits, literal * lits, bool learned);
         clause * mk_clause_core(literal_vector const& lits) { return mk_clause_core(lits.size(), lits.c_ptr()); }
         clause * mk_clause_core(unsigned num_lits, literal * lits) { return mk_clause_core(num_lits, lits, false); }
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index 13780529a..8823c40c5 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -60,6 +60,7 @@ class inc_sat_solver : public solver {
     atom2bool_var       m_map;
     scoped_ptr<bit_blaster_rewriter> m_bb_rewriter;
     tactic_ref          m_preprocess;
+    bool                m_is_cnf;
     unsigned            m_num_scopes;
     sat::literal_vector m_asms;
     goal_ref_buffer     m_subgoals;
@@ -88,6 +89,7 @@ public:
         m_fmls_head(0),
         m_core(m),
         m_map(m),
+        m_is_cnf(true),
         m_num_scopes(0),
         m_unknown("no reason given"),
         m_internalized_converted(false), 
@@ -262,7 +264,19 @@ public:
     void assert_expr_core2(expr * t, expr * a) override {        
         if (a) {
             m_asmsf.push_back(a);
-            assert_expr_core(m.mk_implies(a, t));
+            if (m_is_cnf && is_literal(t) && is_literal(a)) {
+                assert_expr_core(m.mk_or(::mk_not(m, a), t));
+            }
+            else if (m_is_cnf && m.is_or(t) && is_clause(t) && is_literal(a)) {
+                expr_ref_vector args(m);
+                args.push_back(::mk_not(m, a));
+                args.append(to_app(t)->get_num_args(), to_app(t)->get_args());
+                assert_expr_core(m.mk_or(args.size(), args.c_ptr()));
+            }
+            else {
+                m_is_cnf = false;
+                assert_expr_core(m.mk_implies(a, t));
+            }
         }
         else {
             assert_expr_core(t);
@@ -272,6 +286,7 @@ public:
     ast_manager& get_manager() const override { return m; }
     void assert_expr_core(expr * t) override {
         TRACE("goal2sat", tout << mk_pp(t, m) << "\n";);
+        m_is_cnf &= is_clause(t);
         m_fmls.push_back(t);
     }
     void set_produce_models(bool f) override {}
@@ -545,7 +560,12 @@ private:
         SASSERT(!g->proofs_enabled());
         TRACE("sat", m_solver.display(tout); g->display(tout););
         try {
-            (*m_preprocess)(g, m_subgoals);
+            if (m_is_cnf) {
+                m_subgoals.push_back(g.get());
+            }
+            else {
+                (*m_preprocess)(g, m_subgoals);
+            }
         }
         catch (tactic_exception & ex) {
             IF_VERBOSE(0, verbose_stream() << "exception in tactic " << ex.msg() << "\n";);
@@ -705,6 +725,25 @@ private:
         }
     }
 
+    bool is_literal(expr* n) {
+        return is_uninterp_const(n) || (m.is_not(n, n) && is_uninterp_const(n));
+    }
+
+    bool is_clause(expr* fml) {
+        if (is_literal(fml)) {
+            return true;
+        }
+        if (!m.is_or(fml)) {
+            return false;
+        }
+        for (expr* n : *to_app(fml)) {
+            if (!is_literal(n)) {
+                return false;
+            }
+        }
+        return true;
+    }
+
     lbool internalize_formulas() {
         if (m_fmls_head == m_fmls.size()) {
             return l_true;
@@ -712,7 +751,8 @@ private:
         dep2asm_t dep2asm;
         goal_ref g = alloc(goal, m, true, false); // models, maybe cores are enabled
         for (unsigned i = m_fmls_head ; i < m_fmls.size(); ++i) {
-            g->assert_expr(m_fmls[i].get());
+            expr* fml = m_fmls.get(i);
+            g->assert_expr(fml);
         }
         lbool res = internalize_goal(g, dep2asm, false);
         if (res != l_undef) {
diff --git a/src/sat/tactic/atom2bool_var.cpp b/src/sat/tactic/atom2bool_var.cpp
index b79eaa251..cd6ab776d 100644
--- a/src/sat/tactic/atom2bool_var.cpp
+++ b/src/sat/tactic/atom2bool_var.cpp
@@ -38,9 +38,13 @@ void atom2bool_var::mk_var_inv(app_ref_vector & var2expr) const {
 }
 
 sat::bool_var atom2bool_var::to_bool_var(expr * n) const {
-    sat::bool_var v = sat::null_bool_var;
-    m_mapping.find(n, v);
-    return v;
+    unsigned idx = m_id2map.get(n->get_id(), UINT_MAX);
+    if (idx == UINT_MAX) {
+        return sat::null_bool_var;
+    }
+    else {
+        return m_mapping[idx].m_value;
+    }
 }
 
 struct collect_boolean_interface_proc {
diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp
index 5dea80f5e..c79068298 100644
--- a/src/smt/smt_context_pp.cpp
+++ b/src/smt/smt_context_pp.cpp
@@ -200,6 +200,7 @@ namespace smt {
             out << "current assignment:\n";
             for (literal lit : m_assigned_literals) {
                 display_literal(out, lit);
+                if (!is_relevant(lit)) out << " n ";
                 out << ": ";
                 display_verbose(out, m_manager, 1, &lit, m_bool_var2expr.c_ptr());
                 out << "\n";
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index f3a3e9238..55adc8370 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -482,12 +482,12 @@ namespace smt {
 
     template<typename Ext>
     void theory_arith<Ext>::mk_idiv_mod_axioms(expr * dividend, expr * divisor) {
+        th_rewriter & s  = get_context().get_rewriter();
         if (!m_util.is_zero(divisor)) {
             ast_manager & m = get_manager();
             // if divisor is zero, then idiv and mod are uninterpreted functions.
             expr_ref div(m), mod(m), zero(m), abs_divisor(m), one(m);
             expr_ref eqz(m), eq(m), lower(m), upper(m);
-            th_rewriter & s  = get_context().get_rewriter();
             div         = m_util.mk_idiv(dividend, divisor);
             mod         = m_util.mk_mod(dividend, divisor);
             zero        = m_util.mk_int(0);
@@ -508,6 +508,17 @@ namespace smt {
             mk_axiom(eqz, upper, !m_util.is_numeral(abs_divisor));
             rational k;
             context& ctx = get_context();
+
+            if (!m_util.is_numeral(divisor)) {
+                // (=> (> y 0) (<= (* y (div x y)) x))
+                // (=> (< y 0) ???)
+                expr_ref div_ge(m), div_non_pos(m);
+                div_ge = m_util.mk_ge(m_util.mk_sub(dividend, m_util.mk_mul(divisor, div)), zero);
+                s(div_ge);
+                div_non_pos = m_util.mk_le(divisor, zero);
+                mk_axiom(div_non_pos, div_ge, false);
+            }
+
             (void)ctx;
             if (m_params.m_arith_enum_const_mod && m_util.is_numeral(divisor, k) &&
                 k.is_pos() && k < rational(8)) {
@@ -542,6 +553,7 @@ namespace smt {
                 }
 #endif
             }
+
 #if 0
             // e-matching is too restrictive for multiplication.
             // also suffers from use-after free so formulas have to be pinned in solver.
diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp
index 6e1626cc1..8db1df26b 100644
--- a/src/smt/theory_bv.cpp
+++ b/src/smt/theory_bv.cpp
@@ -53,6 +53,7 @@ namespace smt {
         unsigned bv_size      = get_bv_size(n);
         context & ctx         = get_context();
         literal_vector & bits = m_bits[v];
+        TRACE("bv", tout << "v" << v << "\n";);
         bits.reset();
         for (unsigned i = 0; i < bv_size; i++) {
             app * bit  = mk_bit2bool(owner, i);
@@ -77,6 +78,7 @@ namespace smt {
         context & ctx    = get_context();
         SASSERT(!ctx.b_internalized(n));
         
+        TRACE("bv", tout << "bit2bool: " << mk_pp(n, ctx.get_manager()) << "\n";);
         expr* first_arg = n->get_arg(0);
 
         if (!ctx.e_internalized(first_arg)) {
@@ -94,23 +96,30 @@ namespace smt {
             // This will also force the creation of all bits for x.
             enode * first_arg_enode = ctx.get_enode(first_arg);
             get_var(first_arg_enode);
+#if 0
+            // constant axiomatization moved to catch all case in the end of function.
+
             // numerals are not blasted into bit2bool, so we do this directly.
             rational val;
             unsigned sz;
             if (!ctx.b_internalized(n) && m_util.is_numeral(first_arg, val, sz)) {
+                
+                TRACE("bv", tout << "bit2bool constants\n";);
                 theory_var v = first_arg_enode->get_th_var(get_id());
                 app* owner = first_arg_enode->get_owner();
                 for (unsigned i = 0; i < sz; ++i) {
-                    ctx.internalize(mk_bit2bool(owner, i), true);
+                    app* e = mk_bit2bool(owner, i);
+                    ctx.internalize(e, true);
                 }
                 m_bits[v].reset();
                 rational bit;                
                 for (unsigned i = 0; i < sz; ++i) {
                     div(val, rational::power_of_two(i), bit);
                     mod(bit, rational(2), bit);
-                    m_bits[v].push_back(bit.is_zero()?false_literal:true_literal);
+                    m_bits[v].push_back(bit.is_zero()?false_literal:true_literal);                                        
                 }
             }
+#endif
         }
          
         enode * arg      = ctx.get_enode(first_arg);
@@ -135,6 +144,19 @@ namespace smt {
             SASSERT(a->m_occs == 0);
             a->m_occs = new (get_region()) var_pos_occ(v_arg, idx);
         }
+        // axiomatize bit2bool on constants.
+        rational val;
+        unsigned sz;
+        if (m_util.is_numeral(first_arg, val, sz)) {
+            rational bit;
+            unsigned idx = n->get_decl()->get_parameter(0).get_int();
+            div(val, rational::power_of_two(idx), bit);
+            mod(bit, rational(2), bit);
+            literal lit = ctx.get_literal(n);
+            if (bit.is_zero()) lit.neg();
+            ctx.mark_as_relevant(lit);
+            ctx.mk_th_axiom(get_id(), 1, &lit);
+        }
     }
 
     void theory_bv::process_args(app * n) {
@@ -602,8 +624,8 @@ namespace smt {
             num *= numeral(2);
         }
         expr_ref sum(m_autil.mk_add(sz, args.c_ptr()), m);
-        arith_rewriter arw(m);
-        ctx.get_rewriter()(sum);
+		th_rewriter rw(m);
+        rw(sum);
         literal l(mk_eq(n, sum, false));
         TRACE("bv", 
               tout << mk_pp(n, m) << "\n";
@@ -622,7 +644,9 @@ namespace smt {
         context& ctx = get_context();
         process_args(n);
         mk_enode(n);
-        mk_bits(ctx.get_enode(n)->get_th_var(get_id()));
+        theory_var v = ctx.get_enode(n)->get_th_var(get_id()); 
+        mk_bits(v);
+
         if (!ctx.relevancy()) {
             assert_int2bv_axiom(n);
         }
@@ -1179,7 +1203,7 @@ namespace smt {
                 m_prop_queue.push_back(var_pos(curr->m_var, curr->m_idx));
                 curr = curr->m_next;
             }
-            TRACE("bv", tout << m_prop_queue.size() << "\n";);
+            TRACE("bv", tout << "prop queue size: " << m_prop_queue.size() << "\n";);
             propagate_bits();
         }
     }
@@ -1196,7 +1220,7 @@ namespace smt {
 
             literal_vector & bits = m_bits[v];
             literal bit           = bits[idx];
-            lbool   val           = ctx.get_assignment(bit); 
+            lbool   val           = ctx.get_assignment(bit);            
             if (val == l_undef) {
                 continue;
             }
@@ -1213,6 +1237,7 @@ namespace smt {
                 SASSERT(bit != ~bit2);
                 lbool   val2             = ctx.get_assignment(bit2);
                 TRACE("bv_bit_prop", tout << "propagating #" << get_enode(v2)->get_owner_id() << "[" << idx << "] = " << val2 << "\n";);
+                TRACE("bv", tout << bit << " " << bit2 << "\n";);
                 
                 if (val != val2) {
                     literal consequent = bit2;
diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp
index de86ef7e3..dea698f3f 100644
--- a/src/smt/theory_pb.cpp
+++ b/src/smt/theory_pb.cpp
@@ -723,10 +723,11 @@ namespace smt {
             ineqs = alloc(ptr_vector<ineq>);
             m_var_infos[lit.var()].m_lit_watch[lit.sign()] = ineqs;
         }
-        for (auto* c1 : *ineqs) {
-            //if (c1 == c) return;
-            SASSERT (c1 != c);
-        }
+        DEBUG_CODE(
+            for (auto* c1 : *ineqs) {
+                //if (c1 == c) return;
+                SASSERT (c1 != c);
+            });
         ineqs->push_back(c);
     }
 
@@ -965,9 +966,9 @@ namespace smt {
         justification* js = nullptr;
         c.inc_propagations(*this);
         if (!resolve_conflict(c, lits)) {
-			if (proofs_enabled()) {
-				js = alloc(theory_lemma_justification, get_id(), ctx, lits.size(), lits.c_ptr());
-			}
+            if (proofs_enabled()) {
+                js = alloc(theory_lemma_justification, get_id(), ctx, lits.size(), lits.c_ptr());
+            }
             ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, nullptr);
         }
         SASSERT(ctx.inconsistent());
@@ -1194,10 +1195,15 @@ namespace smt {
         // perform unit propagation
         if (maxsum >= c.mpz_k() && maxsum - mininc < c.mpz_k()) { 
             literal_vector& lits = get_unhelpful_literals(c, true);
+            // for (literal lit : lits) SASSERT(ctx.get_assignment(lit) == l_true);
             lits.push_back(c.lit());
+            // SASSERT(ctx.get_assignment(c.lit()) == l_true);
             for (unsigned i = 0; i < sz; ++i) {
-                DEBUG_CODE(validate_assign(c, lits, c.lit(i)););
-                add_assign(c, lits, c.lit(i));                               
+                literal lit = c.lit(i);
+                if (ctx.get_assignment(lit) == l_undef) {
+                    DEBUG_CODE(validate_assign(c, lits, lit););
+                    add_assign(c, lits, c.lit(i));               
+                }
             }
         }
     }
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 283bd4e57..10b2992fe 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -251,7 +251,7 @@ void theory_seq::init(context* ctx) {
     m_arith_value.init(ctx);
 }
 
-#define TRACEFIN(s) { TRACE("seq", tout << ">>" << s << "\n";); IF_VERBOSE(10, verbose_stream() << s << "\n"); }
+#define TRACEFIN(s) { TRACE("seq", tout << ">>" << s << "\n";); IF_VERBOSE(11, verbose_stream() << s << "\n"); }
 
 
 final_check_status theory_seq::final_check_eh() {
@@ -262,6 +262,7 @@ final_check_status theory_seq::final_check_eh() {
     m_new_propagation = false;
     TRACE("seq", display(tout << "level: " << get_context().get_scope_level() << "\n"););
     TRACE("seq_verbose", get_context().display(tout););
+
     if (simplify_and_solve_eqs()) {
         ++m_stats.m_solve_eqs;
         TRACEFIN("solve_eqs");
@@ -3495,12 +3496,11 @@ bool theory_seq::add_itos_val_axiom(expr* e) {
 }
 
 bool theory_seq::add_stoi_val_axiom(expr* e) {
-    context& ctx = get_context();
     expr* n = nullptr;
     rational val, val2;
     VERIFY(m_util.str.is_stoi(e, n));    
 
-    TRACE("seq", tout << mk_pp(e, m) << " " << ctx.get_scope_level () << " " << get_length(n, val) << " " << val << "\n";);
+    TRACE("seq", tout << mk_pp(e, m) << " " << get_context().get_scope_level () << " " << get_length(n, val) << " " << val << "\n";);
 
     if (m_util.str.is_itos(n)) {
         return false;
@@ -3537,7 +3537,7 @@ expr_ref theory_seq::digit2int(expr* ch) {
 
 
 
-// n >= 0 & len(e) = k => is_digit(e_i) for i = 0..k-1
+// n >= 0 & len(e) >= i + 1 => is_digit(e_i) for i = 0..k-1
 // n >= 0 & len(e) = k => n = sum 10^i*digit(e_i)
 // n < 0  & len(e) = k => \/_i ~is_digit(e_i) for i = 0..k-1
 // 10^k <= n < 10^{k+1}-1 => len(e) = k
@@ -3557,7 +3557,9 @@ void theory_seq::add_si_axiom(expr* e, expr* n, unsigned k) {
     for (unsigned i = 0; i < k; ++i) {
         ith_char = mk_nth(e, m_autil.mk_int(i));
         literal isd = is_digit(ith_char);
-        add_axiom(~len_eq_k, ~ge0, isd);
+        literal len_ge_i1 = mk_literal(m_autil.mk_ge(len, m_autil.mk_int(i+1)));
+        add_axiom(~len_ge_i1, ~ge0, isd);
+        digits.push_back(~isd);
         chars.push_back(m_util.str.mk_unit(ith_char));
         nums.push_back(digit2int(ith_char));
     }        
@@ -3951,7 +3953,6 @@ model_value_proc * theory_seq::mk_value(enode * n, model_generator & mg) {
 
 app* theory_seq::mk_value(app* e) {
     expr_ref result(m);
-    context& ctx = get_context();
     e = get_ite_value(e);
     result = m_rep.find(e);
 
@@ -4260,6 +4261,9 @@ void theory_seq::deque_axiom(expr* n) {
     else if (m_util.str.is_at(n)) {
         add_at_axiom(n);
     }
+    else if (m_util.str.is_nth(n)) {
+        add_nth_axiom(n);
+    }
     else if (m_util.str.is_string(n)) {
         add_elim_string_axiom(n);
     }
@@ -4586,7 +4590,12 @@ void theory_seq::propagate_in_re(expr* n, bool is_true) {
 
     IF_VERBOSE(11, verbose_stream() << mk_pp(s, m) << " in " << re << "\n");
     eautomaton* a = get_automaton(re);
-    if (!a) return;
+    if (!a) {
+        std::stringstream strm;
+        strm << "expression " << re << " does not correspond to a supported regular expression";
+        TRACE("seq", tout << strm.str() << "\n";);
+        throw default_exception(strm.str());
+    }
 
     m_s_in_re.push_back(s_in_re(lit, s, re, a));
     m_trail_stack.push(push_back_vector<theory_seq, vector<s_in_re>>(m_s_in_re));
@@ -4705,7 +4714,6 @@ bool theory_seq::lower_bound2(expr* _e, rational& lo) {
 
 
 bool theory_seq::get_length(expr* e, rational& val) const {
-    context& ctx = get_context();
     rational val1;
     expr_ref len(m), len_val(m);
     expr* e1 = nullptr, *e2 = nullptr;
@@ -4960,6 +4968,17 @@ void theory_seq::add_at_axiom(expr* e) {
     add_axiom(~i_ge_len_s, mk_eq(e, emp, false));
 }
 
+void theory_seq::add_nth_axiom(expr* e) {
+    expr* s = nullptr, *i = nullptr;
+    rational n;
+    zstring str;
+    VERIFY(m_util.str.is_nth(e, s, i));
+    if (m_util.str.is_string(s, str) && m_autil.is_numeral(i, n) && n.is_unsigned() && n.get_unsigned() < str.length()) {
+        app_ref ch(m_util.str.mk_char(str[n.get_unsigned()]), m);
+        add_axiom(mk_eq(ch, e, false));
+    }
+}
+
 
 /*
     lit => s = (nth s 0) ++ (nth s 1) ++ ... ++ (nth s idx) ++ (tail s idx)
@@ -5426,6 +5445,7 @@ void theory_seq::relevant_eh(app* n) {
         m_util.str.is_replace(n) ||
         m_util.str.is_extract(n) ||
         m_util.str.is_at(n) ||
+        m_util.str.is_nth(n) ||
         m_util.str.is_empty(n) ||
         m_util.str.is_string(n) ||
         m_util.str.is_itos(n) || 
@@ -5562,14 +5582,9 @@ void theory_seq::propagate_accept(literal lit, expr* acc) {
         propagate_lit(nullptr, 1, &lit, false_literal);
         return;
     }
-    if (_idx.get_unsigned() > m_max_unfolding_depth && 
-        m_max_unfolding_lit != null_literal && ctx.get_scope_level() > 0) {
-        propagate_lit(nullptr, 1, &lit, ~m_max_unfolding_lit);
-        return;
-    }
+
 
     expr_ref len = mk_len(e);
-
     literal_vector lits;
     lits.push_back(~lit);
     if (aut->is_final_state(src)) {
@@ -5579,9 +5594,11 @@ void theory_seq::propagate_accept(literal lit, expr* acc) {
     else {
         propagate_lit(nullptr, 1, &lit, ~mk_literal(m_autil.mk_le(len, idx)));
     }
+
+
     eautomaton::moves mvs;
     aut->get_moves_from(src, mvs);
-    TRACE("seq", tout << mvs.size() << "\n";);
+    TRACE("seq", tout << mk_pp(acc, m) << " #moves " << mvs.size() << "\n";);
     for (auto const& mv : mvs) {
         expr_ref nth = mk_nth(e, idx);
         expr_ref t = mv.t()->accept(nth);
@@ -5590,6 +5607,11 @@ void theory_seq::propagate_accept(literal lit, expr* acc) {
         lits.push_back(step);
     }
     ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
+
+    if (_idx.get_unsigned() > m_max_unfolding_depth && 
+        m_max_unfolding_lit != null_literal && ctx.get_scope_level() > 0) {
+        propagate_lit(nullptr, 1, &lit, ~m_max_unfolding_lit);
+    }
 }
 
 void theory_seq::add_theory_assumptions(expr_ref_vector & assumptions) {
diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
index 9925188b6..242d24e4f 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -575,6 +575,7 @@ namespace smt {
 
         expr_ref add_elim_string_axiom(expr* n);
         void add_at_axiom(expr* n);
+        void add_nth_axiom(expr* n);
         void add_in_re_axiom(expr* n);
         void add_itos_axiom(expr* n);
         void add_stoi_axiom(expr* n);
diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 02801648a..75ca7cf47 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -1682,10 +1682,10 @@ namespace smt {
         expr_ref i1(mk_int_var("i1"), m);
         expr_ref result(mk_str_var("result"), m);
 
-        expr * replaceS;
-        expr * replaceT;
-        expr * replaceTPrime;
-        u.str.is_replace(ex, replaceS, replaceT, replaceTPrime);
+        expr * replaceS = nullptr;
+        expr * replaceT = nullptr;
+        expr * replaceTPrime = nullptr;
+        VERIFY(u.str.is_replace(ex, replaceS, replaceT, replaceTPrime));
 
         // t empty => result = (str.++ t' s)
         expr_ref emptySrcAst(ctx.mk_eq_atom(replaceT, mk_string("")), m);
@@ -4851,6 +4851,7 @@ namespace smt {
     bool theory_str::get_arith_value(expr* e, rational& val) const {
          context& ctx = get_context();
          ast_manager & m = get_manager();
+         (void)m;
          if (!ctx.e_internalized(e)) {
              return false;
          }
@@ -8255,6 +8256,7 @@ namespace smt {
 
     void theory_str::check_eqc_concat_concat(std::set<expr*> & eqc_concat_lhs, std::set<expr*> & eqc_concat_rhs) {
         ast_manager & m = get_manager();
+        (void)m;
 
         int hasCommon = 0;
         if (!eqc_concat_lhs.empty() && !eqc_concat_rhs.empty()) {
diff --git a/src/util/debug.cpp b/src/util/debug.cpp
index 3e40e412c..1b85fbbbb 100644
--- a/src/util/debug.cpp
+++ b/src/util/debug.cpp
@@ -56,17 +56,17 @@ void finalize_debug() {
 
 void enable_debug(const char * tag) {
     init_debug_table();
-    g_enabled_debug_tags->insert(const_cast<char *>(tag));
+    g_enabled_debug_tags->insert(tag);
 }
 
 void disable_debug(const char * tag) {
     init_debug_table();
-    g_enabled_debug_tags->erase(const_cast<char *>(tag));
+    g_enabled_debug_tags->erase(tag);
 }
 
 bool is_debug_enabled(const char * tag) {
     init_debug_table();
-    return g_enabled_debug_tags->contains(const_cast<char *>(tag));
+    return g_enabled_debug_tags->contains(tag);
 }
 
 #if !defined(_WINDOWS) && !defined(NO_Z3_DEBUGGER)
diff --git a/src/util/debug.h b/src/util/debug.h
index 536df4588..613328013 100644
--- a/src/util/debug.h
+++ b/src/util/debug.h
@@ -44,6 +44,17 @@ bool assertions_enabled();
 #define DEBUG_CODE(CODE) ((void) 0)
 #endif
 
+#ifdef __APPLE__
+#include <TargetConditionals.h>
+#if !TARGET_OS_OSX
+#define NO_Z3_DEBUGGER
+#endif
+#endif
+
+#ifdef __EMSCRIPTEN__
+#define NO_Z3_DEBUGGER
+#endif
+
 #ifdef NO_Z3_DEBUGGER
 #define INVOKE_DEBUGGER() exit(ERR_INTERNAL_FATAL)
 #else
diff --git a/src/util/str_hashtable.h b/src/util/str_hashtable.h
index e12cdc7a7..111d54ac8 100644
--- a/src/util/str_hashtable.h
+++ b/src/util/str_hashtable.h
@@ -28,7 +28,7 @@ struct str_hash_proc {
     unsigned operator()(char const * s) const { return string_hash(s, static_cast<unsigned>(strlen(s)), 17); } 
 };
 struct str_eq_proc { bool operator()(char const * s1, char const * s2) const { return strcmp(s1, s2) == 0; } }; 
-typedef ptr_hashtable<char, str_hash_proc, str_eq_proc> str_hashtable;
+typedef ptr_hashtable<const char, str_hash_proc, str_eq_proc> str_hashtable;
 
 #endif /* STR_HASHTABLE_H_ */
 
diff --git a/src/util/symbol.cpp b/src/util/symbol.cpp
index 90b245e6c..3f0e7c967 100644
--- a/src/util/symbol.cpp
+++ b/src/util/symbol.cpp
@@ -35,20 +35,19 @@ class internal_symbol_table {
 public:
 
     char const * get_str(char const * d) {
-        char * result;
+        const char * result;
         #pragma omp critical (cr_symbol) 
         {
-        char * r_d = const_cast<char *>(d);
         str_hashtable::entry * e;
-        if (m_table.insert_if_not_there_core(r_d, e)) {
+        if (m_table.insert_if_not_there_core(d, e)) {
             // new entry
             size_t l   = strlen(d);
             // store the hash-code before the string
             size_t * mem = static_cast<size_t*>(m_region.allocate(l + 1 + sizeof(size_t)));
             *mem = e->get_hash();
             mem++;
-            result = reinterpret_cast<char*>(mem);
-            memcpy(result, d, l+1);
+            result = reinterpret_cast<const char*>(mem);
+            memcpy(mem, d, l+1);
             // update the entry with the new ptr.
             e->set_data(result);
         }
diff --git a/src/util/trace.cpp b/src/util/trace.cpp
index 68437ab92..e4b210021 100644
--- a/src/util/trace.cpp
+++ b/src/util/trace.cpp
@@ -38,7 +38,7 @@ void finalize_trace() {
 }
 
 void enable_trace(const char * tag) {
-    get_enabled_trace_tags().insert(const_cast<char *>(tag));
+    get_enabled_trace_tags().insert(tag);
 }
 
 void enable_all_trace(bool flag) {
@@ -46,12 +46,12 @@ void enable_all_trace(bool flag) {
 }
 
 void disable_trace(const char * tag) {
-    get_enabled_trace_tags().erase(const_cast<char *>(tag));
+    get_enabled_trace_tags().erase(tag);
 }
 
 bool is_trace_enabled(const char * tag) {
     return g_enable_all_trace_tags || 
-        (g_enabled_trace_tags && get_enabled_trace_tags().contains(const_cast<char *>(tag)));
+        (g_enabled_trace_tags && get_enabled_trace_tags().contains(tag));
 }
 
 void close_trace() {