Merge branch 'master' of https://github.com/z3prover/z3

src/api/api_opt.cpp

@@ -139,7 +139,9 @@ extern "C" {
                 r = to_optimize_ptr(o)->optimize();
             }
             catch (z3_exception& ex) {
-                mk_c(c)->handle_exception(ex);
+                if (!mk_c(c)->m().canceled()) {
+                    mk_c(c)->handle_exception(ex);
+                }
                 r = l_undef;
             }
             // to_optimize_ref(d).cleanup();

src/api/api_solver.cpp

@@ -361,7 +361,9 @@ extern "C" {
             }
             catch (z3_exception & ex) {
                 to_solver_ref(s)->set_reason_unknown(eh);
-                mk_c(c)->handle_exception(ex);
+                if (!mk_c(c)->m().canceled()) {
+                    mk_c(c)->handle_exception(ex);
+                }
                 return Z3_L_UNDEF;
             }
         }

src/api/python/z3/z3.py

@@ -9826,6 +9826,14 @@ def String(name, ctx=None):
     ctx = _get_ctx(ctx)
     return SeqRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), StringSort(ctx).ast), ctx)
 
+def SubString(s, offset, length):
+    """Extract substring or subsequence starting at offset"""
+    return Extract(s, offset, length)
+
+def SubSeq(s, offset, length):
+    """Extract substring or subsequence starting at offset"""
+    return Extract(s, offset, length)
+
 def Strings(names, ctx=None):
     """Return a tuple of String constants. """
     ctx = _get_ctx(ctx)

src/muz/fp/datalog_parser.cpp

@@ -108,7 +108,9 @@ public:
 #endif
     }
     ~line_reader() {
-        fclose(m_file);
+        if (m_file != nullptr){
+            fclose(m_file);
+        }
     }
 
     bool operator()() { return m_ok; }

src/smt/smt_solver.cpp

@@ -61,10 +61,13 @@ namespace smt {
             smt_solver * result = alloc(smt_solver, m, p, m_logic);
             smt::kernel::copy(m_context, result->m_context);
 
-            for (auto & kv : m_name2assertion) 
+            for (auto & kv : m_name2assertion) { 
-                result->m_name2assertion.insert(translator(kv.m_key),
+                expr* val = translator(kv.m_value);
-                                                translator(kv.m_value));
+                expr* t = translator(kv.m_key);
-
+                result->m_name2assertion.insert(t, val);
+                result->solver_na2as::assert_expr(val, t);
+                m.inc_ref(val);
+            }
             return result;
         }
 

src/solver/combined_solver.cpp

@@ -59,7 +59,8 @@ private:
     ref<solver>          m_solver2;
     // We delay sending assertions to solver 2
     // This is relevant for big benchmarks that are meant to be solved
-    // by a non-incremental solver. 
+    // by a non-incremental solver.                                                 );
+
     bool                 m_solver2_initialized;
 
     bool                 m_ignore_solver1;
@@ -137,6 +138,7 @@ public:
     }
 
     solver* translate(ast_manager& m, params_ref const& p) override {
+        TRACE("solver", tout << "translate\n";);
         solver* s1 = m_solver1->translate(m, p);
         solver* s2 = m_solver2->translate(m, p);
         combined_solver* r = alloc(combined_solver, s1, s2, p);

src/util/lp/permutation_matrix.h

@@ -132,7 +132,7 @@ class permutation_matrix : public tail_matrix<T, X> {
 
         unsigned size() const { return static_cast<unsigned>(m_rev.size()); }
 
-        unsigned * values() const { return m_permutation; }
+        unsigned * values() const { return m_permutation.c_ptr(); }
 
         void resize(unsigned size) {
             unsigned old_size = m_permutation.size();