Merge branch 'jfleisher/nightlyallowunsigned' into jfleisher/devIntellitest

cmake/target_arch_detect.cpp

@@ -5,6 +5,8 @@
 #error CMAKE_TARGET_ARCH_i686
 #elif defined(__x86_64__) || defined(_M_X64)
 #error CMAKE_TARGET_ARCH_x86_64
+#elif defined(__ARM_ARCH)
+#error CMAKE_TARGET_ARCH_arm
 #else
 #error CMAKE_TARGET_ARCH_unknown
 #endif

examples/java/JavaExample.java

@@ -1868,7 +1868,7 @@ class JavaExample
             }
         } else
         {
-            System.out.println("BUG, the constraints are satisfiable.");
+            System.out.println("BUG, the constraints are not satisfiable.");
         }
     }
 

examples/python/efsmt.py

@@ -5,43 +5,34 @@ from z3.z3util import get_vars
 Modified from the example in  pysmt
 https://github.com/pysmt/pysmt/blob/97088bf3b0d64137c3099ef79a4e153b10ccfda7/examples/efsmt.py
 '''
-def efsmt(y, phi, maxloops=None):
+
-    """Solving exists x. forall y. phi(x, y)"""
+def efsmt(ys, phi, maxloops = None):
-    vars = get_vars(phi)
+    """Solving exists xs. forall ys. phi(x, y)"""
-    x = [item for item in vars if item not in y]
+    xs = [x for x in get_vars(phi) if x not in ys]
-    esolver = Solver()
+    E = Solver()
-    fsolver = Solver()
+    F = Solver()
-    esolver.add(BoolVal(True))
+    E.add(BoolVal(True))
     loops = 0
     while maxloops is None or loops <= maxloops:
         loops += 1
-        eres = esolver.check()
+        eres = E.check()
-        if eres == unsat:
+        if eres == sat:
-            return unsat
+            emodel = E.model()
-        else:
+            sub_phi = substitute(phi, [(x, emodel.eval(x, True)) for x in xs])
-            emodel = esolver.model()
+            F.push()
-            tau = [emodel.eval(var, True) for var in x]
+            F.add(Not(sub_phi))
-            sub_phi = phi
+            fres = F.check()
-            for i in range(len(x)):
+            if fres == sat:
-                sub_phi = simplify(substitute(sub_phi, (x[i], tau[i])))
+                fmodel = F.model()
-            fsolver.add(Not(sub_phi))
+                sub_phi = substitute(phi, [(y, fmodel.eval(y, True)) for y in ys])
-            if fsolver.check() == sat:
+                E.add(sub_phi)
-                fmodel = fsolver.model()
-                sigma = [fmodel.eval(v, True) for v in y]
-                sub_phi = phi
-                for j in range(len(y)):
-                    sub_phi = simplify(substitute(sub_phi, (y[j], sigma[j])))
-                esolver.add(sub_phi)
             else:
-                return sat
+                return fres, [(x, emodel.eval(x, True)) for x in xs]
+            F.pop()
+        else:
+            return eres
     return unknown
 
-
+x, y, z = Reals("x y z")
-def test():
+print(efsmt([y], Implies(And(y > 0, y < 10), y - 2 * x < 7)))
-    x, y, z = Reals("x y z")
+print(efsmt([y], And(y > 3, x == 1)))
-    fmla = Implies(And(y > 0, y < 10), y - 2 * x < 7)
-    fmlb = And(y > 3, x == 1)
-    print(efsmt([y], fmla))
-    print(efsmt([y], fmlb))
-    
-test()

examples/python/visitor.py

@@ -17,13 +17,71 @@ def visitor(e, seen):
             yield e
         return
 
-x, y = Ints('x y')
+def modify(e, fn):
-fml = x + x + y > 2 
+    seen = {}
-seen = {}
+    def visit(e):
-for e in visitor(fml, seen):
+        if e in seen:
-    if is_const(e) and e.decl().kind() == Z3_OP_UNINTERPRETED:
+            pass
-        print("Variable", e)
+        elif fn(e) is not None:
-    else:
+            seen[e] = fn(e)
-        print(e)
+        elif is_and(e):
-    
+            chs = [visit(ch) for ch in e.children()]
+            seen[e] = And(chs)
+        elif is_or(e):
+            chs = [visit(ch) for ch in e.children()]
+            seen[e] = Or(chs)
+        elif is_app(e):
+            chs = [visit(ch) for ch in e.children()]
+            seen[e] = e.decl()(chs)
+        elif is_quantifier(e):
+            # Note: does not work for Lambda that requires a separate case
+            body = visit(e.body())            
+            is_forall = e.is_forall()
+            num_pats = e.num_patterns()
+            pats = (Pattern * num_pats)()
+            for i in range(num_pats):
+                pats[i] = e.pattern(i).ast
+
+            num_decls = e.num_vars()
+            sorts = (Sort * num_decls)()
+            names = (Symbol * num_decls)()
+            for i in range(num_decls):
+                sorts[i] = e.var_sort(i).ast
+                names[i] = to_symbol(e.var_name(i), e.ctx)
+            r = QuantifierRef(Z3_mk_quantifier(e.ctx_ref(), is_forall, e.weight(), num_pats, pats, num_decls, sorts, names, body.ast), e.ctx)
+            seen[e] = r            
+        else:
+            seen[e] = e
+        return seen[e]
+    return visit(e)
+
+if __name__ == "__main__":
+    x, y = Ints('x y')
+    fml = x + x + y > 2 
+    seen = {}
+    for e in visitor(fml, seen):
+        if is_const(e) and e.decl().kind() == Z3_OP_UNINTERPRETED:
+            print("Variable", e)
+        else:
+            print(e)
+
+    s = SolverFor("HORN")
+    inv = Function('inv', IntSort(), IntSort(), BoolSort())
+    i, ip, j, jp = Ints('i ip j jp')
+    s.add(ForAll([i, j], Implies(i == 0, inv(i, j))))
+    s.add(ForAll([i, ip, j, jp], Implies(And(inv(i, j), i < 10, ip == i + 1), inv(ip, jp))))
+    s.add(ForAll([i, j], Implies(And(inv(i, j), i >= 10),  i == 10)))
+
+    a0, a1, a2 = Ints('a0 a1 a2')
+    b0, b1, b2 = Ints('b0 b1 b2')
+    x = Var(0, IntSort())
+    y = Var(1, IntSort())
+    template = And(a0 + a1*x + a2*y >= 0, b0 + b1*x + b2*y >= 0)    
+    def update(e):
+        if is_app(e) and eq(e.decl(), inv):
+            return substitute_vars(template, (e.arg(0)), e.arg(1))
+        return None
+    for f in s.assertions():
+        f_new = modify(f, update)
+        print(f_new)
 

scripts/nightly.yaml

@@ -4,7 +4,7 @@ variables:
   Minor: '8'
   Patch: '16'
   NightlyVersion: $(Major).$(Minor).$(Patch).$(Build.BuildId)-$(Build.DefinitionName)
-  MacFlags: 'CXXFLAGS="-arch arm64 -arch x86_64" LINK_EXTRA_FLAGS="-arch arm64 -arch x86_64" SLINK_EXTRA_FLAGS="-arch arm64 -arch x86_64" FPMATH_ENABLED=False'
+  MacFlags: 'CXXFLAGS="-arch x86_64" LINK_EXTRA_FLAGS="-arch x86_64" SLINK_EXTRA_FLAGS="-arch x86_64"'
 
 stages:
 - stage: Build
@@ -24,6 +24,7 @@ stages:
         artifactName: 'Mac'
         targetPath: $(Build.ArtifactStagingDirectory)
 
+
   - job: Ubuntu
     displayName: "Ubuntu build"
     pool:
@@ -193,6 +194,7 @@ stages:
         patchVersion: $(Patch)
         arguments: 'pack $(Agent.TempDirectory)\package\out\Microsoft.Z3.sym.nuspec -Version $(NightlyVersion) -OutputDirectory $(Build.ArtifactStagingDirectory) -Verbosity detailed -Symbols -SymbolPackageFormat snupkg -BasePath $(Agent.TempDirectory)\package\out' 
     - task: EsrpCodeSigning@1
+      continueOnError: true
       displayName: 'Sign Package'
       inputs:
         ConnectedServiceName: 'z3-esrp-signing-2'
@@ -220,6 +222,7 @@ stages:
         MaxConcurrency: '50'
         MaxRetryAttempts: '5'
     - task: EsrpCodeSigning@1
+      continueOnError: true 
       displayName: 'Sign Symbol Package'
       inputs:
         ConnectedServiceName: 'z3-esrp-signing-2'
@@ -296,6 +299,7 @@ stages:
         patchVersion: $(Patch)
         arguments: 'pack $(Agent.TempDirectory)\package\out\Microsoft.Z3.x86.sym.nuspec -Version $(NightlyVersion) -OutputDirectory $(Build.ArtifactStagingDirectory) -Verbosity detailed -Symbols -SymbolPackageFormat snupkg -BasePath $(Agent.TempDirectory)\package\out' 
     - task: EsrpCodeSigning@1
+      continueOnError: true 
       displayName: 'Sign Package'
       inputs:
         ConnectedServiceName: 'z3-esrp-signing-2'
@@ -323,6 +327,7 @@ stages:
         MaxConcurrency: '50'
         MaxRetryAttempts: '5'
     - task: EsrpCodeSigning@1
+      continueOnError: true 
       displayName: 'Sign Symbol Package'
       inputs:
         ConnectedServiceName: 'z3-esrp-signing-2'
@@ -392,6 +397,7 @@ stages:
         artifactName: 'Python packages'
         targetPath: src/api/python/dist
 
+
 - stage: Deployment
   jobs:
   - job: Deploy

src/api/c++/z3++.h

@@ -2333,7 +2333,7 @@ namespace z3 {
 
     inline expr pble(expr_vector const& es, int const* coeffs, int bound) {
         assert(es.size() > 0);
-        context& ctx = es[0].ctx();
+        context& ctx = es[0u].ctx();
         array<Z3_ast> _es(es);
         Z3_ast r = Z3_mk_pble(ctx, _es.size(), _es.ptr(), coeffs, bound);
         ctx.check_error();
@@ -2341,7 +2341,7 @@ namespace z3 {
     }
     inline expr pbge(expr_vector const& es, int const* coeffs, int bound) {
         assert(es.size() > 0);
-        context& ctx = es[0].ctx();
+        context& ctx = es[0u].ctx();
         array<Z3_ast> _es(es);
         Z3_ast r = Z3_mk_pbge(ctx, _es.size(), _es.ptr(), coeffs, bound);
         ctx.check_error();
@@ -2349,7 +2349,7 @@ namespace z3 {
     }
     inline expr pbeq(expr_vector const& es, int const* coeffs, int bound) {
         assert(es.size() > 0);
-        context& ctx = es[0].ctx();
+        context& ctx = es[0u].ctx();
         array<Z3_ast> _es(es);
         Z3_ast r = Z3_mk_pbeq(ctx, _es.size(), _es.ptr(), coeffs, bound);
         ctx.check_error();
@@ -2357,7 +2357,7 @@ namespace z3 {
     }
     inline expr atmost(expr_vector const& es, unsigned bound) {
         assert(es.size() > 0);
-        context& ctx = es[0].ctx();
+        context& ctx = es[0u].ctx();
         array<Z3_ast> _es(es);
         Z3_ast r = Z3_mk_atmost(ctx, _es.size(), _es.ptr(), bound);
         ctx.check_error();
@@ -2365,7 +2365,7 @@ namespace z3 {
     }
     inline expr atleast(expr_vector const& es, unsigned bound) {
         assert(es.size() > 0);
-        context& ctx = es[0].ctx();
+        context& ctx = es[0u].ctx();
         array<Z3_ast> _es(es);
         Z3_ast r = Z3_mk_atleast(ctx, _es.size(), _es.ptr(), bound);
         ctx.check_error();
@@ -2373,7 +2373,7 @@ namespace z3 {
     }
     inline expr sum(expr_vector const& args) {
         assert(args.size() > 0);
-        context& ctx = args[0].ctx();
+        context& ctx = args[0u].ctx();
         array<Z3_ast> _args(args);
         Z3_ast r = Z3_mk_add(ctx, _args.size(), _args.ptr());
         ctx.check_error();
@@ -2382,7 +2382,7 @@ namespace z3 {
 
     inline expr distinct(expr_vector const& args) {
         assert(args.size() > 0);
-        context& ctx = args[0].ctx();
+        context& ctx = args[0u].ctx();
         array<Z3_ast> _args(args);
         Z3_ast r = Z3_mk_distinct(ctx, _args.size(), _args.ptr());
         ctx.check_error();
@@ -2411,14 +2411,14 @@ namespace z3 {
         Z3_ast r;
         assert(args.size() > 0);
         if (args.size() == 1) {
-            return args[0];
+            return args[0u];
         }
-        context& ctx = args[0].ctx();
+        context& ctx = args[0u].ctx();
         array<Z3_ast> _args(args);
-        if (Z3_is_seq_sort(ctx, args[0].get_sort())) {
+        if (Z3_is_seq_sort(ctx, args[0u].get_sort())) {
             r = Z3_mk_seq_concat(ctx, _args.size(), _args.ptr());
         }
-        else if (Z3_is_re_sort(ctx, args[0].get_sort())) {
+        else if (Z3_is_re_sort(ctx, args[0u].get_sort())) {
             r = Z3_mk_re_concat(ctx, _args.size(), _args.ptr());
         }
         else {
@@ -2448,7 +2448,7 @@ namespace z3 {
     inline expr mk_xor(expr_vector const& args) {
         if (args.empty())
             return args.ctx().bool_val(false);
-        expr r = args[0];
+        expr r = args[0u];
         for (unsigned i = 1; i < args.size(); ++i)
             r = r ^ args[i];
         return r;
@@ -2771,7 +2771,7 @@ namespace z3 {
                 assert(!m_end && !m_empty);
                 m_cube = m_solver.cube(m_vars, m_cutoff);
                 m_cutoff = 0xFFFFFFFF;
-                if (m_cube.size() == 1 && m_cube[0].is_false()) {
+                if (m_cube.size() == 1 && m_cube[0u].is_false()) {
                     m_cube = z3::expr_vector(m_solver.ctx());
                     m_end = true;
                 }
@@ -3005,7 +3005,7 @@ namespace z3 {
         }
         array<Z3_tactic> buffer(n);
         for (unsigned i = 0; i < n; ++i) buffer[i] = tactics[i];
-        return tactic(tactics[0].ctx(), Z3_tactic_par_or(tactics[0].ctx(), n, buffer.ptr()));
+        return tactic(tactics[0u].ctx(), Z3_tactic_par_or(tactics[0u].ctx(), n, buffer.ptr()));
     }
 
     inline tactic par_and_then(tactic const & t1, tactic const & t2) {
@@ -3804,7 +3804,7 @@ namespace z3 {
     }
     inline expr re_intersect(expr_vector const& args) {
         assert(args.size() > 0);
-        context& ctx = args[0].ctx();
+        context& ctx = args[0u].ctx();
         array<Z3_ast> _args(args);
         Z3_ast r = Z3_mk_re_intersect(ctx, _args.size(), _args.ptr());
         ctx.check_error();

src/api/dotnet/NativeFuncInterp.cs

@@ -85,13 +85,14 @@ namespace Microsoft.Z3
 
             for (uint j = 0; j < numEntries; ++j)
             {
-                var entry = Native.Z3_func_interp_get_entry(nCtx, fi, j);
+                var ntvEntry = Native.Z3_func_interp_get_entry(nCtx, fi, j);
-                Native.Z3_func_entry_inc_ref(nCtx, entry);
+                Entries[j] = new Entry();
+                Native.Z3_func_entry_inc_ref(nCtx, ntvEntry);
                 Entries[j].Arguments = new Z3_ast[numArgs];
                 for (uint i = 0; i < numArgs; ++i)
-                    Entries[j].Arguments[i] = Native.Z3_func_entry_get_arg(nCtx, entry, i);
+                    Entries[j].Arguments[i] = Native.Z3_func_entry_get_arg(nCtx, ntvEntry, i);
-                Entries[j].Result = Native.Z3_func_entry_get_value(nCtx, entry);
+                Entries[j].Result = Native.Z3_func_entry_get_value(nCtx, ntvEntry);
-                Native.Z3_func_entry_dec_ref(nCtx, entry);
+                Native.Z3_func_entry_dec_ref(nCtx, ntvEntry);
             }
 
             Native.Z3_func_interp_dec_ref(nCtx, fi);

src/ast/rewriter/bv_rewriter.cpp

@@ -37,6 +37,7 @@ void bv_rewriter::updt_local_params(params_ref const & _p) {
     m_extract_prop = p.bv_extract_prop();
     m_ite2id = p.bv_ite2id();
     m_le_extra = p.bv_le_extra();
+    m_le2extract = p.bv_le2extract();
     set_sort_sums(p.bv_sort_ac());
 }
 
@@ -577,7 +578,7 @@ br_status bv_rewriter::mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref
             result = m().mk_eq(a, m_util.mk_numeral(numeral(0), bv_sz));
             return BR_REWRITE1;
         }
-        else if (first_non_zero < bv_sz - 1) {
+        else if (first_non_zero < bv_sz - 1 && m_le2extract) {
             result = m().mk_and(m().mk_eq(m_mk_extract(bv_sz - 1, first_non_zero + 1, a), m_util.mk_numeral(numeral(0), bv_sz - first_non_zero - 1)),
                                 m_util.mk_ule(m_mk_extract(first_non_zero, 0, a), m_mk_extract(first_non_zero, 0, b)));
             return BR_REWRITE3;

src/ast/rewriter/bv_rewriter.h

@@ -62,6 +62,7 @@ class bv_rewriter : public poly_rewriter<bv_rewriter_core> {
     bool       m_extract_prop;
     bool       m_bvnot_simpl;
     bool       m_le_extra;
+    bool       m_le2extract;
 
     bool is_zero_bit(expr * x, unsigned idx);
 

src/cmd_context/cmd_context.cpp

@@ -1815,6 +1815,9 @@ void cmd_context::display_model(model_ref& mdl) {
 }
 
 void cmd_context::add_declared_functions(model& mdl) {
+    model_params p;
+    if (!p.user_functions())
+        return;
     for (auto const& kv : m_func_decls) {
         func_decl* f = kv.m_value.first();
         if (f->get_family_id() == null_family_id && !mdl.has_interpretation(f)) {

src/math/lp/lp_dual_simplex_def.h

@@ -217,14 +217,14 @@ template <typename T, typename X> void lp_dual_simplex<T, X>::fill_costs_bounds_
         m_can_enter_basis[j] = true;
         this->set_scaled_cost(j);
         this->m_lower_bounds[j] = numeric_traits<T>::zero();
-        this->m_upper_bounds[j] =numeric_traits<T>::one();
+        this->m_upper_bounds[j] = numeric_traits<T>::one();
         break;
     }
     case column_type::free_column: {
         m_can_enter_basis[j] = true;
         this->set_scaled_cost(j);
-        this->m_upper_bounds[j] = free_bound;
+        this->m_upper_bounds[j] =  free_bound;
-        this->m_lower_bounds[j] =  -free_bound;
+        this->m_lower_bounds[j] = -free_bound;
         break;
     }
     case column_type::boxed:

src/model/datatype_factory.cpp

@@ -48,10 +48,8 @@ expr * datatype_factory::get_some_value(sort * s) {
 */
 expr * datatype_factory::get_last_fresh_value(sort * s) {
     expr * val = nullptr;
-    if (m_last_fresh_value.find(s, val)) {
+    if (m_last_fresh_value.find(s, val)) 
-        TRACE("datatype", tout << "cached fresh value: " << mk_pp(val, m_manager) << "\n";);
         return val;
-    }
     value_set * set = get_value_set(s);
     if (set->empty())
         val = get_some_value(s);
@@ -200,7 +198,7 @@ expr * datatype_factory::get_fresh_value(sort * s) {
     if (m_util.is_recursive(s)) {
         while (true) {
             ++num_iterations;
-            TRACE("datatype", tout << mk_pp(get_last_fresh_value(s), m_manager) << "\n";);
+            TRACE("datatype", tout << num_iterations << " " << mk_pp(get_last_fresh_value(s), m_manager) << "\n";);
             ptr_vector<func_decl> const & constructors = *m_util.get_datatype_constructors(s);
             for (func_decl * constructor : constructors) {
                 expr_ref_vector args(m_manager);
@@ -219,7 +217,7 @@ expr * datatype_factory::get_fresh_value(sort * s) {
                         expr * maybe_new_arg = nullptr;
                         if (!m_util.is_datatype(s_arg))
                             maybe_new_arg = m_model.get_fresh_value(s_arg);
-                        else if (num_iterations <= 1)
+                        else if (num_iterations <= 1 || m_util.is_recursive(s_arg))
                             maybe_new_arg = get_almost_fresh_value(s_arg);                        
                         else 
                             maybe_new_arg = get_fresh_value(s_arg);

src/model/model_params.pyg

@@ -5,6 +5,7 @@ def_module_params('model',
                           ('v2', BOOL, False, 'use Z3 version 2.x (x <= 16) pretty printer'),
                           ('compact', BOOL, True, 'try to compact function graph (i.e., function interpretations that are lookup tables)'),
                           ('inline_def', BOOL, False, 'inline local function definitions ignoring possible expansion'),
+                          ('user_functions', BOOL, True, 'include user defined functions in model'),
                           ('completion', BOOL, False, 'enable/disable model completion'),
                           ))
 

src/params/bv_rewriter_params.pyg

@@ -11,5 +11,6 @@ def_module_params(module_name='rewriter',
                           ("bv_extract_prop", BOOL, False, "attempt to partially propagate extraction inwards"),
                           ("bv_not_simpl", BOOL, False, "apply simplifications for bvnot"),
                           ("bv_ite2id", BOOL, False, "rewrite ite that can be simplified to identity"),
-                          ("bv_le_extra", BOOL, False, "additional bu_(u/s)le simplifications")
+                          ("bv_le_extra", BOOL, False, "additional bu_(u/s)le simplifications"),
+                          ("bv_le2extract", BOOL, True, "disassemble bvule to extract")
                           ))

src/qe/qe.cpp

@@ -1484,13 +1484,11 @@ namespace qe {
                   tout << "free: " << m_free_vars << "\n";);
 
             free_vars.append(m_free_vars);
-            if (!m_free_vars.empty() || m_solver.inconsistent()) {
 
-                if (m_fml.get() != m_subfml.get()) {
+            if (m_fml.get() != m_subfml.get()) {
-                    scoped_ptr<expr_replacer> rp = mk_default_expr_replacer(m, false);
+                scoped_ptr<expr_replacer> rp = mk_default_expr_replacer(m, false);
-                    rp->apply_substitution(to_app(m_subfml.get()), fml, m_fml);
+                rp->apply_substitution(to_app(m_subfml.get()), fml, m_fml);
-                    fml = m_fml;
+                fml = m_fml;
-                }
             }
             reset();
             m_solver.pop(1);

src/sat/sat_simplifier.cpp

@@ -652,6 +652,7 @@ namespace sat {
 
     inline void simplifier::propagate_unit(literal l) {
         unsigned old_trail_sz = s.m_trail.size();
+        unsigned num_clauses = s.m_clauses.size();
         s.assign_scoped(l);
         s.propagate_core(false); // must not use propagate(), since s.m_clauses is not in a consistent state.
         if (s.inconsistent())
@@ -672,6 +673,8 @@ namespace sat {
             }
             cs.reset();            
         }
+        for (unsigned i = num_clauses; i < s.m_clauses.size(); ++i) 
+            m_use_list.insert(*s.m_clauses[i]);
     }
 
     void simplifier::elim_lit(clause & c, literal l) {
@@ -1806,6 +1809,8 @@ namespace sat {
     */
     bool simplifier::resolve(clause_wrapper const & c1, clause_wrapper const & c2, literal l, literal_vector & r) {
         CTRACE("resolve_bug", !c1.contains(l), tout << c1 << "\n" << c2 << "\nl: " << l << "\n";);
+        if (m_visited.size() <= 2*s.num_vars())
+            m_visited.resize(2*s.num_vars(), false);
         SASSERT(c1.contains(l));
         SASSERT(c2.contains(~l));
         bool res = true;
@@ -1825,6 +1830,10 @@ namespace sat {
             literal l2 = c2[i];
             if (not_l == l2)
                 continue;
+            if ((~l2).index() >= m_visited.size()) {
+                s.display(std::cout << l2 << " " << s.num_vars() << " " << m_visited.size() << "\n");
+                exit(0);
+            }
             if (m_visited[(~l2).index()]) {
                 res = false;
                 break;

src/sat/smt/array_model.cpp

@@ -24,27 +24,32 @@ namespace array {
 
     void solver::init_model() {
         collect_defaults();
+        collect_selects();
+    }
+
+    void solver::finalize_model(model& mdl) {
+        std::for_each(m_selects_range.begin(), m_selects_range.end(), delete_proc<select_set>());
     }
     
-    bool solver::add_dep(euf::enode* n, top_sort<euf::enode>& dep) { 
+    bool solver::add_dep(euf::enode* n, top_sort<euf::enode>& dep) {
         if (!a.is_array(n->get_expr())) {
             dep.insert(n, nullptr);
             return true;
-        }       
+        }
-        for (euf::enode* p : euf::enode_parents(n->get_root())) {
+        if (a.is_array(n->get_expr())) {
-            if (a.is_default(p->get_expr())) {
+            for (euf::enode* p : euf::enode_parents(n->get_root())) 
+                if (a.is_default(p->get_expr())) 
+                    dep.add(n, p);
+                            
+            for (euf::enode* p : *get_select_set(n)) {
                 dep.add(n, p);
-                continue;
+                for (unsigned i = 1; i < p->num_args(); ++i)
+                    dep.add(n, p->get_arg(i));
             }
-            if (!a.is_select(p->get_expr()))
-                continue;
-            dep.add(n, p);
-            for (unsigned i = 1; i < p->num_args(); ++i)
-                dep.add(n, p->get_arg(i));
         }
         for (euf::enode* k : euf::enode_class(n)) 
             if (a.is_const(k->get_expr())) 
-                dep.add(n, k->get_arg(0)); 
+                dep.add(n, k->get_arg(0));
         theory_var v = get_th_var(n);
         euf::enode* d = get_default(v);
         if (d)
@@ -103,17 +108,27 @@ namespace array {
 
         if (!get_else(v) && fi->get_else())
             set_else(v, fi->get_else());
-        
+
-        for (euf::enode* p : euf::enode_parents(n)) {
+        if (!get_else(v)) {
-            if (a.is_select(p->get_expr()) && p->get_arg(0)->get_root() == n) {
+            expr* else_value = mdl.get_some_value(get_array_range(srt));
-                expr* value = values.get(p->get_root_id(), nullptr);
+            fi->set_else(else_value);
-                if (!value || value == fi->get_else())
+            set_else(v, else_value);
-                    continue;
+        }
-                args.reset();
+
-                for (unsigned i = 1; i < p->num_args(); ++i) 
+        for (euf::enode* p : *get_select_set(n)) {
-                    args.push_back(values.get(p->get_arg(i)->get_root_id()));    
+            expr* value = values.get(p->get_root_id(), nullptr);
-                fi->insert_entry(args.data(), value);
+            if (!value || value == fi->get_else())
+                continue;
+            args.reset();
+            for (unsigned i = 1; i < p->num_args(); ++i) {
+                if (!values.get(p->get_arg(i)->get_root_id())) {
+                    TRACE("array", tout << ctx.bpp(p->get_arg(i)) << "\n");
+                }
+                SASSERT(values.get(p->get_arg(i)->get_root_id()));
             }
+            for (unsigned i = 1; i < p->num_args(); ++i) 
+                args.push_back(values.get(p->get_arg(i)->get_root_id()));    
+            fi->insert_entry(args.data(), value);
         }
         
         TRACE("array", tout << "array-as-function " << ctx.bpp(n) << " := " << mk_pp(f, m) << "\n" << "default " << mk_pp(fi->get_else(), m) << "\n";);
@@ -135,52 +150,103 @@ namespace array {
             return true;
 
         return false;
-#if 0
+    }
-        struct eq {
-            solver& s;
-            eq(solver& s) :s(s) {}
-            bool operator()(euf::enode* n1, euf::enode* n2) const {
-                SASSERT(s.a.is_select(n1->get_expr()));
-                SASSERT(s.a.is_select(n2->get_expr()));
-                for (unsigned i = n1->num_args(); i-- > 1; ) 
-                    if (n1->get_arg(i)->get_root() != n2->get_arg(i)->get_root())
-                        return false;
-                return true;                
-            }
-        };
-        struct hash {
-            solver& s;
-            hash(solver& s) :s(s) {}
-            unsigned operator()(euf::enode* n) const {
-                SASSERT(s.a.is_select(n->get_expr()));
-                unsigned h = 33;
-                for (unsigned i = n->num_args(); i-- > 1; )
-                    h = hash_u_u(h, n->get_arg(i)->get_root_id());
-                return h;
-            }
-        };
-        eq eq_proc(*this);
-        hash hash_proc(*this);
-        hashtable<euf::enode*, hash, eq> table(DEFAULT_HASHTABLE_INITIAL_CAPACITY, hash_proc, eq_proc);
-        euf::enode* p2 = nullptr;
-        auto maps_diff = [&](euf::enode* p, euf::enode* else_, euf::enode* r) {
-            return table.find(p, p2) ? p2->get_root() != r : (else_ && else_ != r);
-        };
-        auto table_diff = [&](euf::enode* r1, euf::enode* r2, euf::enode* else1) {
-            table.reset();
-            for (euf::enode* p : euf::enode_parents(r1))
-                if (a.is_select(p->get_expr()) && r1 == p->get_arg(0)->get_root())
-                    table.insert(p);
-            for (euf::enode* p : euf::enode_parents(r2))
-                if (a.is_select(p->get_expr()) && r2 == p->get_arg(0)->get_root())
-                    if (maps_diff(p, else1, p->get_root()))
-                        return true;
-            return false;
-        };
-        
-        return table_diff(r1, r2, else1) || table_diff(r2, r1, else2);
 
-#endif
+    unsigned solver::sel_hash::operator()(euf::enode * n) const {
+        return get_composite_hash<euf::enode *, sel_khasher, sel_chasher>(n, n->num_args() - 1, sel_khasher(), sel_chasher());
+    }
+
+    bool solver::sel_eq::operator()(euf::enode * n1, euf::enode * n2) const {
+        SASSERT(n1->num_args() == n2->num_args());
+        unsigned num_args = n1->num_args();
+        for (unsigned i = 1; i < num_args; i++) 
+            if (n1->get_arg(i)->get_root() != n2->get_arg(i)->get_root())
+                return false;
+        return true;
+    }
+
+
+    void solver::collect_selects() {
+        int num_vars = get_num_vars();
+
+        m_selects.reset();
+        m_selects_domain.reset();
+        m_selects_range.reset();
+
+        for (theory_var v = 0; v < num_vars; ++v) {
+            euf::enode * r = var2enode(v)->get_root();                
+            if (is_representative(v) && ctx.is_relevant(r)) {
+                for (euf::enode * parent : euf::enode_parents(r)) {
+                    if (parent->get_cg() == parent &&
+                        ctx.is_relevant(parent) &&
+                        a.is_select(parent->get_expr()) &&
+                        parent->get_arg(0)->get_root() == r) {
+                        select_set * s = get_select_set(r);
+                        SASSERT(!s->contains(parent) || (*(s->find(parent)))->get_root() == parent->get_root());
+                        s->insert(parent);
+                    }
+                }
+            }
+        }
+        euf::enode_pair_vector todo;
+        for (euf::enode * r : m_selects_domain)
+            for (euf::enode* sel : *get_select_set(r))
+                propagate_select_to_store_parents(r, sel, todo);
+        for (unsigned qhead = 0; qhead < todo.size(); qhead++) {
+            euf::enode_pair & pair = todo[qhead];
+            euf::enode * r   = pair.first;
+            euf::enode * sel = pair.second;
+            propagate_select_to_store_parents(r, sel, todo);
+        }
+    }
+
+    void solver::propagate_select_to_store_parents(euf::enode* r, euf::enode* sel, euf::enode_pair_vector& todo) {
+        SASSERT(r->get_root() == r);
+        SASSERT(a.is_select(sel->get_expr()));
+        if (!ctx.is_relevant(r)) 
+            return;
+        
+        for (euf::enode * parent : euf::enode_parents(r)) {
+            if (ctx.is_relevant(parent) &&
+                a.is_store(parent->get_expr()) &&
+                parent->get_arg(0)->get_root() == r) {
+                // propagate upward
+                select_set * parent_sel_set = get_select_set(parent);
+                euf::enode * parent_root = parent->get_root();
+                
+                if (parent_sel_set->contains(sel))
+                    continue;
+
+                SASSERT(sel->num_args() + 1 == parent->num_args());
+                    
+                // check whether the sel idx was overwritten by the store
+                unsigned num_args = sel->num_args();
+                unsigned i = 1;
+                for (; i < num_args; i++) {
+                    if (sel->get_arg(i)->get_root() != parent->get_arg(i)->get_root())
+                        break;
+                }
+
+                if (i < num_args) {
+                    SASSERT(!parent_sel_set->contains(sel) || (*(parent_sel_set->find(sel)))->get_root() == sel->get_root());
+                    parent_sel_set->insert(sel);
+                    todo.push_back(std::make_pair(parent_root, sel));
+                }
+            }
+        }
+    }
+
+    solver::select_set* solver::get_select_set(euf::enode* n) {
+        euf::enode * r = n->get_root();
+        select_set * set = nullptr;
+        m_selects.find(r, set);
+        if (set == nullptr) {
+            set = alloc(select_set);
+            m_selects.insert(r, set);
+            m_selects_domain.push_back(r);
+            m_selects_range.push_back(set);
+        }
+        return set;
     }
 
     void solver::collect_defaults() {

src/sat/smt/array_solver.h

@@ -218,11 +218,39 @@ namespace array {
         void pop_core(unsigned n) override;
         
         // models
+        // I need a set of select enodes where select(A,i) = select(B,j) if i->get_root() == j->get_root()
+        struct sel_khasher {
+            unsigned operator()(euf::enode const * n) const { return 0; }
+        };
+
+        struct sel_chasher {
+            unsigned operator()(euf::enode const * n, unsigned idx) const { 
+                return n->get_arg(idx+1)->get_root()->hash();
+            }
+        };
+        
+        struct sel_hash {
+            unsigned operator()(euf::enode * n) const;
+        };
+
+        struct sel_eq {
+            bool operator()(euf::enode * n1, euf::enode * n2) const;
+        };
+        
+        typedef ptr_hashtable<euf::enode, sel_hash, sel_eq> select_set;
         euf::enode_vector   m_defaults;       // temporary field for model construction
         ptr_vector<expr>    m_else_values;    // 
         svector<int>        m_parents;        // temporary field for model construction
+        obj_map<euf::enode, select_set*>  m_selects;        // mapping from array -> relevant selects
+        ptr_vector<euf::enode>            m_selects_domain; 
+        ptr_vector<select_set>            m_selects_range;
+
         bool must_have_different_model_values(theory_var v1, theory_var v2);
+        select_set* get_select_set(euf::enode* n);
         void collect_defaults();
+        void collect_selects();               // mapping from array -> relevant selects
+        void propagate_select_to_store_parents(euf::enode* r, euf::enode* sel, euf::enode_pair_vector& todo);
+
         void mg_merge(theory_var u, theory_var v);
         theory_var mg_find(theory_var n);
         void set_default(theory_var v, euf::enode* n);
@@ -254,6 +282,7 @@ namespace array {
         void new_diseq_eh(euf::th_eq const& eq) override;
         bool unit_propagate() override;
         void init_model() override;
+        void finalize_model(model& mdl) override;
         bool include_func_interp(func_decl* f) const override { return a.is_ext(f); }
         void add_value(euf::enode* n, model& mdl, expr_ref_vector& values) override;
         bool add_dep(euf::enode* n, top_sort<euf::enode>& dep) override;

src/sat/smt/euf_model.cpp

@@ -63,9 +63,17 @@ namespace euf {
         }
     };
 
+    void solver::save_model(model_ref& mdl) {
+        m_qmodel = mdl;
+    }
+
     void solver::update_model(model_ref& mdl) {
         TRACE("model", tout << "create model\n";);
-        mdl->reset_eval_cache();
+        if (m_qmodel) {
+            mdl = m_qmodel;
+            return;
+        }
+        mdl->reset_eval_cache();        
         for (auto* mb : m_solvers)
             mb->init_model();
         m_values.reset();

src/sat/smt/euf_solver.h

@@ -154,6 +154,7 @@ namespace euf {
         // model building
         expr_ref_vector m_values;
         obj_map<expr, enode*> m_values2root;        
+        model_ref m_qmodel;
         bool include_func_interp(func_decl* f);
         void register_macros(model& mdl);
         void dependencies2values(user_sort& us, deps_t& deps, model_ref& mdl);
@@ -395,6 +396,7 @@ namespace euf {
         relevancy& get_relevancy() { return m_relevancy; }
 
         // model construction
+        void save_model(model_ref& mdl);
         void update_model(model_ref& mdl);
         obj_map<expr, enode*> const& values2root();
         void model_updated(model_ref& mdl);

src/sat/smt/q_mam.cpp

@@ -1893,7 +1893,8 @@ namespace q {
         }
 
         void recycle_enode_vector(enode_vector * v) {
-            m_pool.recycle(v);
+            if (v)
+                m_pool.recycle(v);
         }
 
         void update_max_generation(enode * n, enode * prev) {
@@ -2197,8 +2198,10 @@ namespace q {
             if (curr->num_args() == expected_num_args && ctx.is_relevant(curr))
                 break;
         }
-        if (bp.m_it == bp.m_end)
+        if (bp.m_it == bp.m_end) {
+            recycle_enode_vector(bp.m_to_recycle);
             return nullptr;
+        }
         m_top++;
         update_max_generation(*(bp.m_it), nullptr);
         return *(bp.m_it);

src/sat/smt/q_mbi.cpp

@@ -48,6 +48,7 @@ namespace q {
     lbool mbqi::operator()() {
         lbool result = l_true;
         m_model = nullptr;
+        ctx.save_model(m_model);
         m_instantiations.reset();
         for (sat::literal lit : m_qs.m_universal) {
             quantifier* q = to_quantifier(ctx.bool_var2expr(lit.var()));
@@ -73,6 +74,9 @@ namespace q {
             m_qs.add_clause(~qlit, ~lit);
         }
         m_instantiations.reset();
+        if (result != l_true)
+            m_model = nullptr;
+        ctx.save_model(m_model);
         return result;
     }
 

src/sat/smt/sat_th.h

@@ -188,6 +188,7 @@ namespace euf {
         enode* expr2enode(expr* e) const;
         enode* var2enode(theory_var v) const { return m_var2enode[v]; }
         expr* var2expr(theory_var v) const { return var2enode(v)->get_expr(); }
+        bool is_representative(theory_var v) const { return v == get_representative(v); }
         expr* bool_var2expr(sat::bool_var v) const;
         expr_ref literal2expr(sat::literal lit) const;
         enode* bool_var2enode(sat::bool_var v) const { expr* e = bool_var2expr(v); return e ? expr2enode(e) : nullptr; }

src/sat/tactic/goal2sat.cpp

@@ -405,6 +405,8 @@ struct goal2sat::imp : public sat::sat_internalizer {
             m_result_stack.shrink(old_sz);
         }
         else {
+            if (process_cached(t, root, sign))
+                return;
             SASSERT(num <= m_result_stack.size());
             sat::bool_var k = add_var(false, t);
             sat::literal  l(k, false);
@@ -454,6 +456,8 @@ struct goal2sat::imp : public sat::sat_internalizer {
             m_result_stack.shrink(old_sz);
         }
         else {
+            if (process_cached(t, root, sign))
+                return;
             SASSERT(num <= m_result_stack.size());
             sat::bool_var k = add_var(false, t);
             sat::literal  l(k, false);
@@ -507,6 +511,8 @@ struct goal2sat::imp : public sat::sat_internalizer {
             }
         }
         else {
+            if (process_cached(n, root, sign))
+                return;
             sat::bool_var k = add_var(false, n);
             sat::literal  l(k, false);
             cache(n, l);
@@ -537,6 +543,8 @@ struct goal2sat::imp : public sat::sat_internalizer {
             mk_root_clause(sign ? lit : ~lit);            
         }
         else {
+            if (process_cached(t, root, sign))
+                return;
             sat::bool_var k = add_var(false, t);
             sat::literal  l(k, false);
             cache(t, l);
@@ -567,6 +575,8 @@ struct goal2sat::imp : public sat::sat_internalizer {
             }            
         }
         else {
+            if (process_cached(t, root, sign))
+                return;
             sat::bool_var k = add_var(false, t);
             sat::literal  l(k, false);
             cache(t, l);
@@ -603,6 +613,8 @@ struct goal2sat::imp : public sat::sat_internalizer {
             }                  
         }
         else {
+            if (process_cached(t, root, sign))
+                return;
             sat::bool_var k = add_var(false, t);
             sat::literal  l(k, false);
             if (m.is_xor(t))

src/smt/smt_context.cpp

@@ -29,6 +29,7 @@ Revision History:
 #include "ast/proofs/proof_checker.h"
 #include "ast/ast_util.h"
 #include "ast/well_sorted.h"
+#include "model/model_params.hpp"
 #include "model/model.h"
 #include "model/model_pp.h"
 #include "smt/smt_context.h"
@@ -205,7 +206,7 @@ namespace smt {
         ast_translation tr(src_ctx.m, m, false);
         for (unsigned i = 0; i < src_ctx.m_user_propagator->get_num_vars(); ++i) {
             app* e = src_ctx.m_user_propagator->get_expr(i);
-            m_user_propagator->add_expr(tr(e));
+            m_user_propagator->add_expr(tr(e), true);
         }
     }
 
@@ -4638,7 +4639,8 @@ namespace smt {
     }
 
     void context::add_rec_funs_to_model() {
-        if (m_model)
+        model_params p;
+        if (m_model && p.user_functions())
             m_model->add_rec_funs();
     }
 

src/smt/smt_context.h

@@ -1729,7 +1729,7 @@ namespace smt {
         void user_propagate_register_expr(expr* e) {
             if (!m_user_propagator) 
                 throw default_exception("user propagator must be initialized");
-            m_user_propagator->add_expr(e);
+            m_user_propagator->add_expr(e, true);
         }
 
         void user_propagate_register_created(user_propagator::created_eh_t& r) {

src/smt/theory_arith.h

@@ -602,9 +602,11 @@ namespace smt {
         void add_row_entry(unsigned r_id, numeral const & coeff, theory_var v);
         uint_set& row_vars();
         class scoped_row_vars;
-        
+
+        void check_app(expr* e, expr* n);
         void internalize_internal_monomial(app * m, unsigned r_id);
         theory_var internalize_add(app * n);
+        theory_var internalize_sub(app * n);
         theory_var internalize_mul_core(app * m);
         theory_var internalize_mul(app * m);
         theory_var internalize_div(app * n);

src/smt/theory_arith_core.h

@@ -302,6 +302,44 @@ namespace smt {
         }
     }
 
+    template<typename Ext>
+    void theory_arith<Ext>::check_app(expr* e, expr* n) {
+        if (is_app(e))
+            return;        
+        std::ostringstream strm;
+        strm << mk_pp(n, m) << " contains a " << (is_var(e) ? "free variable":"quantifier");
+        throw default_exception(strm.str());        
+    }
+    
+
+    template<typename Ext>
+    theory_var theory_arith<Ext>::internalize_sub(app * n) {
+        VERIFY(m_util.is_sub(n));
+        bool first = true;
+        unsigned r_id = mk_row();
+        scoped_row_vars _sc(m_row_vars, m_row_vars_top);
+        theory_var v;
+        for (expr* arg : *n) {
+            check_app(arg, n);
+            v = internalize_term_core(to_app(arg));
+            if (first)
+                add_row_entry<true>(r_id, numeral::one(), v);
+            else
+                add_row_entry<false>(r_id, numeral::one(), v);
+            first = false;
+        }
+        enode * e = mk_enode(n);
+        v = e->get_th_var(get_id());
+        if (v == null_theory_var) {
+            v = mk_var(e);
+            add_row_entry<false>(r_id, numeral::one(), v);
+            init_row(r_id);
+        }
+        else
+            del_row(r_id);
+        return v;
+    }
+    
     /**
        \brief Internalize a polynomial (+ h t). Return an alias for the monomial, that is,
        a variable v such that v = (+ h t) is a new row in the tableau.
@@ -314,11 +352,7 @@ namespace smt {
         unsigned r_id = mk_row();
         scoped_row_vars _sc(m_row_vars, m_row_vars_top);
         for (expr* arg : *n) {
-            if (is_var(arg)) {
+            check_app(arg, n);
-                std::ostringstream strm;
-                strm << mk_pp(n, m) << " contains a free variable";
-                throw default_exception(strm.str());
-            }
             internalize_internal_monomial(to_app(arg), r_id);
         }
         enode * e = mk_enode(n);
@@ -383,11 +417,7 @@ namespace smt {
             }
             unsigned r_id = mk_row();
             scoped_row_vars _sc(m_row_vars, m_row_vars_top);
-            if (is_var(arg1)) {
+            check_app(arg1, m);
-                std::ostringstream strm;
-                strm << mk_pp(m, get_manager()) << " contains a free variable";
-                throw default_exception(strm.str());
-            }
             if (reflection_enabled())
                 internalize_term_core(to_app(arg0));
             theory_var v = internalize_mul_core(to_app(arg1));
@@ -749,7 +779,6 @@ namespace smt {
                 return e->get_th_var(get_id());
         }
 
-        SASSERT(!m_util.is_sub(n));
         SASSERT(!m_util.is_uminus(n));
 
         if (m_util.is_add(n))
@@ -770,6 +799,8 @@ namespace smt {
             return internalize_to_int(n);
         else if (m_util.is_numeral(n))
             return internalize_numeral(n);
+        else if (m_util.is_sub(n))
+            return internalize_sub(n);
         if (m_util.is_power(n)) {
             // unsupported
             found_unsupported_op(n);

src/smt/theory_seq.cpp

@@ -1498,8 +1498,8 @@ void theory_seq::add_length(expr* l) {
     TRACE("seq", tout << mk_bounded_pp(e, m, 2) << "\n";);
     m_length.push_back(l);
     m_has_length.insert(e);
-    m_trail_stack.push(insert_obj_trail<expr>(m_has_length, e));
     m_trail_stack.push(push_back_vector<expr_ref_vector>(m_length));
+    m_trail_stack.push(insert_obj_trail<expr>(m_has_length, e));
 }
 
 /**
@@ -1542,8 +1542,8 @@ bool theory_seq::add_length_to_eqc(expr* e) {
         expr* o = n->get_expr();
         if (!has_length(o)) {
             expr_ref len(m_util.str.mk_length(o), m);
-            ensure_enode(len);
             add_length(len);
+            ensure_enode(len);
             change = true;
         }
         n = n->get_next();

src/smt/theory_user_propagator.cpp

@@ -24,7 +24,8 @@ using namespace smt;
 
 theory_user_propagator::theory_user_propagator(context& ctx):
     theory(ctx, ctx.get_manager().mk_family_id(user_propagator::plugin::name())),
-    m_var2expr(ctx.get_manager())
+    m_var2expr(ctx.get_manager()),
+    m_to_add(ctx.get_manager())
 {}
 
 theory_user_propagator::~theory_user_propagator() {
@@ -33,13 +34,15 @@ theory_user_propagator::~theory_user_propagator() {
 
 void theory_user_propagator::force_push() {
     for (; m_num_scopes > 0; --m_num_scopes) {
+        flet<bool> _pushing(m_push_popping, true);
         theory::push_scope_eh();
-        m_push_eh(m_user_context);
         m_prop_lim.push_back(m_prop.size());
+        m_to_add_lim.push_back(m_to_add.size());
+        m_push_eh(m_user_context);
     }
 }
 
-void theory_user_propagator::add_expr(expr* term) {
+void theory_user_propagator::add_expr(expr* term, bool ensure_enode) {
     force_push();
     expr_ref r(m);
     expr* e = term;
@@ -52,7 +55,7 @@ void theory_user_propagator::add_expr(expr* term) {
         e = r;
         ctx.mark_as_relevant(eq.get());
     }
-    enode* n = ensure_enode(e);
+    enode* n = ensure_enode ? this->ensure_enode(e) : ctx.get_enode(e);
     if (is_attached_to_var(n))
         return;
 
@@ -82,6 +85,7 @@ void theory_user_propagator::propagate_cb(
     expr* conseq) {
     CTRACE("user_propagate", ctx.lit_internalized(conseq) && ctx.get_assignment(ctx.get_literal(conseq)) == l_true,
            ctx.display(tout << "redundant consequence: " << mk_pp(conseq, m) << "\n"));
+
     expr_ref _conseq(conseq, m);
     ctx.get_rewriter()(conseq, _conseq);
     if (ctx.lit_internalized(_conseq) && ctx.get_assignment(ctx.get_literal(_conseq)) == l_true) 
@@ -90,7 +94,10 @@ void theory_user_propagator::propagate_cb(
 }
 
 void theory_user_propagator::register_cb(expr* e) {
-    add_expr(e);
+    if (m_push_popping)
+        m_to_add.push_back(e);
+    else
+        add_expr(e, true);
 }
 
 theory * theory_user_propagator::mk_fresh(context * new_ctx) {
@@ -144,25 +151,29 @@ void theory_user_propagator::new_fixed_eh(theory_var v, expr* value, unsigned nu
      }
 }
 
-void theory_user_propagator::push_scope_eh() {
+void theory_user_propagator::push_scope_eh() {    
     ++m_num_scopes;
 }
 
 void theory_user_propagator::pop_scope_eh(unsigned num_scopes) {
+    flet<bool> _popping(m_push_popping, true);
     unsigned n = std::min(num_scopes, m_num_scopes);
     m_num_scopes -= n;
     num_scopes -= n;
     if (num_scopes == 0)
         return;
-    m_pop_eh(m_user_context, num_scopes);
     theory::pop_scope_eh(num_scopes);
     unsigned old_sz = m_prop_lim.size() - num_scopes;
     m_prop.shrink(m_prop_lim[old_sz]);
     m_prop_lim.shrink(old_sz);
+    old_sz = m_to_add_lim.size() - num_scopes;
+    m_to_add.shrink(m_to_add_lim[old_sz]);
+    m_to_add_lim.shrink(old_sz);
+    m_pop_eh(m_user_context, num_scopes);
 }
 
 bool theory_user_propagator::can_propagate() {
-    return m_qhead < m_prop.size();
+    return m_qhead < m_prop.size() || !m_to_add.empty();
 }
 
 void theory_user_propagator::propagate_consequence(prop_info const& prop) {
@@ -215,10 +226,19 @@ void theory_user_propagator::propagate_new_fixed(prop_info const& prop) {
 
 void theory_user_propagator::propagate() {
     TRACE("user_propagate", tout << "propagating queue head: " << m_qhead << " prop queue: " << m_prop.size() << "\n");
-    if (m_qhead == m_prop.size())
+    if (m_qhead == m_prop.size() && m_to_add_qhead == m_to_add.size())
         return;
     force_push();
-    unsigned qhead = m_qhead;
+    
+    unsigned qhead = m_to_add_qhead;
+    if (qhead < m_to_add.size()) {
+        for (; qhead < m_to_add.size(); ++qhead)
+            add_expr(m_to_add.get(qhead), true);
+        ctx.push_trail(value_trail<unsigned>(m_to_add_qhead));
+        m_to_add_qhead = qhead;
+    }
+
+    qhead = m_qhead;
     while (qhead < m_prop.size() && !ctx.inconsistent()) {
         auto const& prop = m_prop[qhead];
         if (prop.m_var == null_theory_var)
@@ -243,7 +263,7 @@ bool theory_user_propagator::internalize_term(app* term)  {
     if (term->get_family_id() == get_id() && !ctx.e_internalized(term)) 
         ctx.mk_enode(term, true, false, true);
     
-    add_expr(term);
+    add_expr(term, false);
     
     if (!m_created_eh)
         throw default_exception("You have to register a created event handler for new terms if you track them");

src/smt/theory_user_propagator.h

@@ -78,6 +78,10 @@ namespace smt {
         stats                  m_stats;
         expr_ref_vector        m_var2expr;
         unsigned_vector        m_expr2var;
+        bool                   m_push_popping;
+        expr_ref_vector        m_to_add;
+        unsigned_vector        m_to_add_lim;
+        unsigned               m_to_add_qhead = 0;
 
         expr* var2expr(theory_var v) { return m_var2expr.get(v); }
         theory_var expr2var(expr* e) { check_defined(e); return m_expr2var[e->get_id()]; }
@@ -110,7 +114,7 @@ namespace smt {
             m_fresh_eh     = fresh_eh;
         }
 
-        void add_expr(expr* e);
+        void add_expr(expr* e, bool ensure_enode);
 
         void register_final(user_propagator::final_eh_t& final_eh) { m_final_eh = final_eh; }
         void register_fixed(user_propagator::fixed_eh_t& fixed_eh) { m_fixed_eh = fixed_eh; }

src/tactic/arith/bv2real_rewriter.cpp

@@ -17,6 +17,7 @@ Notes:
 
 --*/
 #include "tactic/arith/bv2real_rewriter.h"
+#include "tactic/tactic_exception.h"
 #include "ast/rewriter/rewriter_def.h"
 #include "ast/ast_pp.h"
 #include "ast/for_each_expr.h"
@@ -40,6 +41,7 @@ bv2real_util::bv2real_util(ast_manager& m, rational const& default_root, rationa
     m_pos_le = m.mk_fresh_func_decl("<=","",2,domain,m.mk_bool_sort());
     m_decls.push_back(m_pos_lt);
     m_decls.push_back(m_pos_le);
+    m_max_memory = std::max((1ull << 31ull), 3*memory::get_allocation_size());
 }
 
 bool bv2real_util::is_bv2real(func_decl* f) const {
@@ -178,12 +180,10 @@ void bv2real_util::align_divisors(expr_ref& s1, expr_ref& s2, expr_ref& t1, expr
 expr* bv2real_util::mk_bv_mul(expr* s, expr* t) {
     SASSERT(m_bv.is_bv(s));
     SASSERT(m_bv.is_bv(t));
-    if (is_zero(s)) {
+    if (is_zero(s)) 
         return s;
-    }
+    if (is_zero(t)) 
-    if (is_zero(t)) {
         return t;
-    }    
     expr_ref s1(s, m()), t1(t, m());
     align_sizes(s1, t1);
     unsigned n = m_bv.get_bv_size(t1);
@@ -343,6 +343,10 @@ bool bv2real_util::mk_is_divisible_by(expr_ref& s, rational const& _overflow) {
 }
 
 
+bool bv2real_util::memory_exceeded() const {
+    return m_max_memory <= memory::get_allocation_size();
+}
+
 
 // ---------------------------------------------------------------------
 // bv2real_rewriter
@@ -362,6 +366,11 @@ br_status bv2real_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr *
               tout << mk_pp(args[i], m()) << " ";
           }
           tout << "\n";);
+    
+    if (u().memory_exceeded()) {
+        std::cout << "tactic exception\n";
+        throw tactic_exception("bv2real-memory exceeded");
+    }
     if(f->get_family_id() == m_arith.get_family_id()) {
         switch (f->get_decl_kind()) {
         case OP_NUM:     return BR_FAILED;

src/tactic/arith/bv2real_rewriter.h

@@ -65,6 +65,7 @@ class bv2real_util {
     rational m_default_divisor;
     rational m_max_divisor;
     unsigned m_max_num_bits;
+    uint64_t m_max_memory;
 
     class contains_bv2real_proc;
 
@@ -81,6 +82,8 @@ public:
 
     bool contains_bv2real(expr* e) const;
 
+    bool memory_exceeded() const;
+
     bool mk_bv2real(expr* s, expr* t, rational& d, rational& r, expr_ref& result);
     expr* mk_bv2real_c(expr* s, expr* t, rational const& d, rational const& r);
     expr* mk_bv2real(expr* n, expr* m) { return mk_bv2real_c(n, m, default_divisor(), default_root()); }

src/tactic/arith/nla2bv_tactic.cpp

@@ -100,20 +100,19 @@ class nla2bv_tactic : public tactic {
                 return;
             }
             substitute_vars(g);
-            TRACE("nla2bv", g.display(tout << "substitute vars\n"););
+            TRACE("nla2bv", g.display(tout << "substitute vars\n"));
             reduce_bv2int(g);
             reduce_bv2real(g);
-            TRACE("nla2bv", g.display(tout << "after reduce\n"););
+            TRACE("nla2bv", g.display(tout << "after reduce\n"));
             mc = m_fmc.get();
-            for (unsigned i = 0; i < m_vars.size(); ++i) {
+            for (unsigned i = 0; i < m_vars.size(); ++i) 
-                m_fmc->add(m_vars[i].get(), m_defs[i].get());
+                m_fmc->add(m_vars.get(i), m_defs.get(i));
-            }
             for (unsigned i = 0; i < m_bv2real.num_aux_decls(); ++i) {
                 m_fmc->hide(m_bv2real.get_aux_decl(i));
             }        
             IF_VERBOSE(TACTIC_VERBOSITY_LVL, verbose_stream() << "(nla->bv :sat-preserving " << m_is_sat_preserving << ")\n";);
-            TRACE("nla2bv_verbose", g.display(tout););
+            TRACE("nla2bv_verbose", g.display(tout));
-            TRACE("nla2bv", tout << "Muls: " << count_mul(g) << "\n";);
+            TRACE("nla2bv", tout << "Muls: " << count_mul(g) << "\n");
             g.inc_depth();
             if (!is_sat_preserving())
                 g.updt_prec(goal::UNDER);

src/tactic/tactical.cpp

@@ -336,6 +336,9 @@ public:
                 catch (tactic_exception &) {
                     result.reset();
                 }
+                catch (rewriter_exception&) {
+                    result.reset();
+                }
                 catch (z3_error & ex) {
                     IF_VERBOSE(10, verbose_stream() << "z3 error: " << ex.error_code() << " in or-else\n");
                     throw;
@@ -1019,7 +1022,6 @@ public:
     void operator()(goal_ref const & in, goal_ref_buffer& result) override {
         cancel_eh<reslimit> eh(in->m().limit());
         { 
-            // Warning: scoped_timer is not thread safe in Linux.
             scoped_timer timer(m_timeout, &eh);
             m_t->operator()(in, result);            
         }