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

package/Microsoft.Z3.x64.nuspec

@@ -0,0 +1,22 @@
+<?xml version="1.0" encoding="utf-8"?>
+<package xmlns="http://schemas.microsoft.com/packaging/2010/07/nuspec.xsd">
+    <metadata>
+        <id>Microsoft.Z3.x64</id>
+        <version>$(releaseVersion)</version>
+		<copyright>© Microsoft Corporation. All rights reserved.</copyright>
+		<authors>Microsoft</authors>
+		<owners>Microsoft,Z3Prover</owners>
+		<iconUrl>$(iconUrlFromReleaseCommit)</iconUrl>
+		<projectUrl>https://github.com/Z3Prover/z3</projectUrl>
+		<licenseUrl>$(licenseUrlFromReleaseCommit)</licenseUrl>
+		<repository
+			type="git"
+			url="https://github.com/Z3Prover/z3.git"
+			branch="master"
+			commit="$(releaseCommitHash)"
+		/>
+		<requireLicenseAcceptance>true</requireLicenseAcceptance>
+		<description>Z3 is a constraint/SMT solver and theorem prover from Microsoft Research.</description>
+		<tags>smt constraint solver theorem prover</tags>
+    </metadata>
+</package>

package/Microsoft.Z3.x64.targets

@@ -0,0 +1,10 @@
+<?xml version="1.0" encoding="utf-8"?>
+<Project ToolsVersion="4.0" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
+    <ItemGroup>
+        <None Include="$(MSBuildThisFileDirectory)libz3.dll">
+            <Visible>false</Visible>
+            <Link>libz3.dll</Link>
+            <CopyToOutputDirectory>PreserveNewest</CopyToOutputDirectory>
+        </None>
+    </ItemGroup>
+</Project>

package/PackageCreationDirections.md

@@ -0,0 +1,36 @@
+# Z3 NuGet packaging
+
+## Creation
+
+ 1. After tagging a commit for release, sign Microsoft.Z3.dll and libz3.dll (both x86 and x64 versions) with Microsoft's Authenticode certificate
+ 2. Test the signed DLLs with the `Get-AuthenticodeSignature` PowerShell commandlet
+ 3. Create the following directory structure for the x64 package (for x86, substitute the "x64" strings for "x86" and use x86 DLLs):
+ ```
+ +-- Microsoft.Z3.x64
+ |   +-- Microsoft.Z3.x64.nuspec
+ |   +-- lib
+ |       +-- net40
+ |           +-- Microsoft.Z3.dll
+ |   +-- build
+ |       +-- Microsoft.Z3.x64.targets
+ |       +-- libz3.dll
+ ```
+ 4. Open the nuspec file and fill in the appropriate macro values (note that for all URLs, preserve link integrity by linking to a specific commit):
+    * $(releaseVersion) - the Z3 version being released in this package
+    * $(iconUrlFromReleaseCommit) - URL for the Z3 icon file
+    * $(licenseUrlFromReleaseCommit) - URL for the Z3 repo license
+    * $(releaseCommitHash) - hash of the release commit
+ 5. Run `nuget pack Microsoft.Z3.x64\Microsoft.Z3.x64.nuspec`
+ 6. Test the resulting nupkg file (described below) then submit the package for signing before uploading to NuGet.org
+
+## Testing
+
+ 1. Create a directory on your machine at C:\nuget-test-source
+ 2. Put the Microsoft.Z3.x64.nupkg file in the directory
+ 3. Open Visual Studio 2017, create a new C# project, then right click the project and click "Manage NuGet packages"
+ 4. Add a new package source - your C:\nuget-test-source directory
+ 5. Find the Microsoft.Z3.x64 package, ensuring in preview window that icon is present and all fields correct
+ 6. Install the Microsoft.Z3.x64 package, ensuring you are asked to accept the license
+ 7. Build your project. Check the output directory to ensure both Microsoft.Z3.dll and libz3.dll are present
+ 8. Import Microsoft.Z3 to your project then add a simple line of code like `using (var ctx = new Context()) { }`; build then run your project to ensure the assemblies load properly
+ 

scripts/mk_util.py

@@ -1668,9 +1668,6 @@ class DotNetDLLComponent(Component):
                                 '/noconfig',
                                 '/nostdlib+',
                                 '/reference:mscorlib.dll',
-                                # Under mono this isn't neccessary as mono will search the system
-                                # library paths for libz3.so
-                                '/linkresource:{}.dll'.format(get_component(Z3_DLL_COMPONENT).dll_name),
                                ]
                              )
 

src/api/api_datalog.cpp

@@ -379,10 +379,8 @@ extern "C" {
         for (unsigned i = 0; i < coll.m_rules.size(); ++i) {
             to_fixedpoint_ref(d)->add_rule(coll.m_rules[i].get(), coll.m_names[i]);
         }
-        ptr_vector<expr>::const_iterator it  = ctx.begin_assertions();
+        for (expr * e : ctx.assertions()) {
-        ptr_vector<expr>::const_iterator end = ctx.end_assertions();
+            to_fixedpoint_ref(d)->ctx().assert_expr(e);
-        for (; it != end; ++it) {
-            to_fixedpoint_ref(d)->ctx().assert_expr(*it);
         }
 
         return of_ast_vector(v);

src/api/api_opt.cpp

@@ -124,10 +124,16 @@ extern "C" {
     }
 
 
-    Z3_lbool Z3_API Z3_optimize_check(Z3_context c, Z3_optimize o) {
+    Z3_lbool Z3_API Z3_optimize_check(Z3_context c, Z3_optimize o, unsigned num_assumptions, Z3_ast const assumptions[]) {
         Z3_TRY;
-        LOG_Z3_optimize_check(c, o);
+        LOG_Z3_optimize_check(c, o, num_assumptions, assumptions);
         RESET_ERROR_CODE();
+        for (unsigned i = 0; i < num_assumptions; i++) {
+            if (!is_expr(to_ast(assumptions[i]))) {
+                SET_ERROR_CODE(Z3_INVALID_ARG, "assumption is not an expression");
+                return Z3_L_UNDEF;
+            }
+        }
         lbool r = l_undef;
         cancel_eh<reslimit> eh(mk_c(c)->m().limit());
         unsigned timeout = to_optimize_ptr(o)->get_params().get_uint("timeout", mk_c(c)->get_timeout());
@@ -137,7 +143,9 @@ extern "C" {
             scoped_timer timer(timeout, &eh);
             scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit);
             try {
-                r = to_optimize_ptr(o)->optimize();
+                expr_ref_vector asms(mk_c(c)->m());
+                asms.append(num_assumptions, to_exprs(assumptions));
+                r = to_optimize_ptr(o)->optimize(asms);
             }
             catch (z3_exception& ex) {
                 if (!mk_c(c)->m().canceled()) {
@@ -157,6 +165,22 @@ extern "C" {
         Z3_CATCH_RETURN(Z3_L_UNDEF);
     }
 
+    Z3_ast_vector Z3_API Z3_optimize_get_unsat_core(Z3_context c, Z3_optimize o) {
+        Z3_TRY;
+        LOG_Z3_optimize_get_unsat_core(c, o);
+        RESET_ERROR_CODE();
+        expr_ref_vector core(mk_c(c)->m());
+        to_optimize_ptr(o)->get_unsat_core(core);
+        Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m());
+        mk_c(c)->save_object(v);
+        for (expr* e : core) {
+            v->m_ast_vector.push_back(e);
+        }
+        RETURN_Z3(of_ast_vector(v));
+        Z3_CATCH_RETURN(nullptr);
+    }
+
+
     Z3_string Z3_API Z3_optimize_get_reason_unknown(Z3_context c, Z3_optimize o) {
         Z3_TRY;
         LOG_Z3_optimize_to_string(c, o);
@@ -330,10 +354,8 @@ extern "C" {
             return;
         }
 
-        ptr_vector<expr>::const_iterator it  = ctx->begin_assertions();
+        for (expr * e : ctx->assertions()) {
-        ptr_vector<expr>::const_iterator end = ctx->end_assertions();
+            to_optimize_ptr(opt)->add_hard_constraint(e);
-        for (; it != end; ++it) {
-            to_optimize_ptr(opt)->add_hard_constraint(*it);
         }
     }
 

src/api/api_parsers.cpp

@@ -71,10 +71,8 @@ extern "C" {
             SET_ERROR_CODE(Z3_PARSER_ERROR, errstrm.str().c_str());
             return of_ast_vector(v);
         }
-        ptr_vector<expr>::const_iterator it  = ctx->begin_assertions();
+        for (expr * e : ctx->assertions()) {
-        ptr_vector<expr>::const_iterator end = ctx->end_assertions();
+            v->m_ast_vector.push_back(e);
-        for (; it != end; ++it) {
-            v->m_ast_vector.push_back(*it);
         }
         return of_ast_vector(v);
         Z3_CATCH_RETURN(nullptr);

src/api/api_solver.cpp

@@ -157,10 +157,8 @@ extern "C" {
         bool initialized = to_solver(s)->m_solver.get() != nullptr;
         if (!initialized)
             init_solver(c, s);
-        ptr_vector<expr>::const_iterator it  = ctx->begin_assertions();
+        for (expr * e : ctx->assertions()) {
-        ptr_vector<expr>::const_iterator end = ctx->end_assertions();
+            to_solver_ref(s)->assert_expr(e);
-        for (; it != end; ++it) {
-            to_solver_ref(s)->assert_expr(*it);
         }
         to_solver_ref(s)->set_model_converter(ctx->get_model_converter());
     }

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

@@ -2455,8 +2455,20 @@ namespace z3 {
         void pop() {
             Z3_optimize_pop(ctx(), m_opt);
         }
-        check_result check() { Z3_lbool r = Z3_optimize_check(ctx(), m_opt); check_error(); return to_check_result(r); }
+        check_result check() { Z3_lbool r = Z3_optimize_check(ctx(), m_opt, 0, 0); check_error(); return to_check_result(r); }
+        check_result check(expr_vector const& asms) { 
+            unsigned n = asms.size();
+            array<Z3_ast> _asms(n);
+            for (unsigned i = 0; i < n; i++) {
+                check_context(*this, asms[i]);
+                _asms[i] = asms[i];
+            }
+            Z3_lbool r = Z3_optimize_check(ctx(), m_opt, n, _asms.ptr()); 
+            check_error(); 
+            return to_check_result(r); 
+        }
         model get_model() const { Z3_model m = Z3_optimize_get_model(ctx(), m_opt); check_error(); return model(ctx(), m); }
+        expr_vector unsat_core() const { Z3_ast_vector r = Z3_optimize_get_unsat_core(ctx(), m_opt); check_error(); return expr_vector(ctx(), r); }
         void set(params const & p) { Z3_optimize_set_params(ctx(), m_opt, p); check_error(); }
         expr lower(handle const& h) {
             Z3_ast r = Z3_optimize_get_lower(ctx(), m_opt, h.h());

src/api/dotnet/CMakeLists.txt

@@ -147,11 +147,6 @@ if (DOTNET_TOOLCHAIN_IS_WINDOWS)
     "/nostdlib+"
     "/reference:mscorlib.dll"
   )
-  # FIXME: This flag only works when the working directory of csc.exe is
-  # the directory containing the ``libz3`` target. I can't get this to work
-  # correctly with multi-configuration generators (i.e. Visual Studio) so
-  # just don't set the flag for now.
-  #list(APPEND CSC_FLAGS "/linkresource:$<TARGET_FILE_NAME:libz3>")
 elseif (DOTNET_TOOLCHAIN_IS_MONO)
   # We need to give the assembly a strong name so that it can be installed
   # into the GAC.

src/api/dotnet/Optimize.cs

@@ -183,9 +183,9 @@ namespace Microsoft.Z3
         /// don't use strict inequalities) meets the objectives.
         /// </summary>
         ///
-        public Status Check()
+        public Status Check(params Expr[] assumptions)
         {
-            Z3_lbool r = (Z3_lbool)Native.Z3_optimize_check(Context.nCtx, NativeObject);
+            Z3_lbool r = (Z3_lbool)Native.Z3_optimize_check(Context.nCtx, NativeObject, (uint)assumptions.Length, AST.ArrayToNative(assumptions));
             switch (r)
             {
                 case Z3_lbool.Z3_L_TRUE:
@@ -236,6 +236,25 @@ namespace Microsoft.Z3
             }
         }
 
+        /// <summary>
+        /// The unsat core of the last <c>Check</c>.
+        /// </summary>
+        /// <remarks>
+        /// The unsat core is a subset of <c>assumptions</c>
+        /// The result is empty if <c>Check</c> was not invoked before,
+        /// if its results was not <c>UNSATISFIABLE</c>, or if core production is disabled.
+        /// </remarks>
+        public BoolExpr[] UnsatCore
+        {
+            get
+            {
+                Contract.Ensures(Contract.Result<Expr[]>() != null);
+
+                ASTVector core = new ASTVector(Context, Native.Z3_optimize_get_unsat_core(Context.nCtx, NativeObject));                
+                return core.ToBoolExprArray();
+            }
+        }
+
         /// <summary>
         /// Declare an arithmetical maximization objective.
         /// Return a handle to the objective. The handle is used as

src/api/java/Context.java

@@ -1976,6 +1976,22 @@ public class Context implements AutoCloseable {
     {
         return (SeqExpr) Expr.create(this, Native.mkString(nCtx(), s));
     }
+
+    /**
+     * Convert an integer expression to a string.
+     */
+    public SeqExpr intToString(Expr e) 
+    {
+	return (SeqExpr) Expr.create(this, Native.mkIntToStr(nCtx(), e.getNativeObject()));
+    }
+
+    /**
+     * Convert an integer expression to a string.
+     */
+    public IntExpr stringToInt(Expr e)  
+    {
+	return (IntExpr) Expr.create(this, Native.mkStrToInt(nCtx(), e.getNativeObject()));
+    }
     
     /**
      * Concatenate sequences.

src/api/java/Optimize.java

@@ -161,9 +161,23 @@ public class Optimize extends Z3Object {
      * Produce a model that (when the objectives are bounded and 
      * don't use strict inequalities) meets the objectives.
      **/
-    public Status Check()
+    public Status Check(Expr... assumptions)
     {
-        Z3_lbool r = Z3_lbool.fromInt(Native.optimizeCheck(getContext().nCtx(), getNativeObject()));
+        Z3_lbool r;
+        if (assumptions == null) {
+          r = Z3_lbool.fromInt(
+              Native.optimizeCheck(
+                  getContext().nCtx(), 
+                  getNativeObject(), 0, null));
+        }
+        else {
+          r = Z3_lbool.fromInt(
+              Native.optimizeCheck(
+                  getContext().nCtx(), 
+                  getNativeObject(), 
+                  assumptions.length, 
+                  AST.arrayToNative(assumptions)));
+        }
         switch (r) {
             case Z3_L_TRUE:
                 return Status.SATISFIABLE;
@@ -209,6 +223,21 @@ public class Optimize extends Z3Object {
         }
     }
 
+    /**
+     * The unsat core of the last {@code Check}.
+     * Remarks:  The unsat core
+     * is a subset of {@code Assumptions} The result is empty if
+     * {@code Check} was not invoked before, if its results was not
+     * {@code UNSATISFIABLE}, or if core production is disabled. 
+     * 
+     * @throws Z3Exception
+     **/
+    public BoolExpr[] getUnsatCore()
+    {
+        ASTVector core = new ASTVector(getContext(), Native.optimizeGetUnsatCore(getContext().nCtx(), getNativeObject()));        
+        return core.ToBoolExprArray();
+    }
+
     /**
      *  Declare an arithmetical maximization objective.
      *  Return a handle to the objective. The handle is used as

src/api/ml/z3.ml

@@ -1947,7 +1947,7 @@ struct
   let minimize (x:optimize) (e:Expr.expr) = mk_handle x (Z3native.optimize_minimize (gc x) x e)
 
   let check (x:optimize) =
-    let r = lbool_of_int (Z3native.optimize_check (gc x) x) in
+    let r = lbool_of_int (Z3native.optimize_check (gc x) x) 0 [] in
     match r with
     | L_TRUE -> Solver.SATISFIABLE
     | L_FALSE -> Solver.UNSATISFIABLE

src/api/python/z3/z3.py

@@ -7311,10 +7311,15 @@ class Optimize(Z3PPObject):
         """restore to previously created backtracking point"""
         Z3_optimize_pop(self.ctx.ref(), self.optimize)
 
-    def check(self):
+    def check(self, *assumptions):
         """Check satisfiability while optimizing objective functions."""
-        return CheckSatResult(Z3_optimize_check(self.ctx.ref(), self.optimize))
+        assumptions = _get_args(assumptions)
-
+        num = len(assumptions)
+        _assumptions = (Ast * num)()
+        for i in range(num):
+            _assumptions[i] = assumptions[i].as_ast()
+        return CheckSatResult(Z3_optimize_check(self.ctx.ref(), self.optimize, num, _assumptions))
+    
     def reason_unknown(self):
         """Return a string that describes why the last `check()` returned `unknown`."""
         return Z3_optimize_get_reason_unknown(self.ctx.ref(), self.optimize)
@@ -7326,6 +7331,9 @@ class Optimize(Z3PPObject):
         except Z3Exception:
             raise Z3Exception("model is not available")
 
+    def unsat_core(self):
+        return AstVector(Z3_optimize_get_unsat_core(self.ctx.ref(), self.optimize), self.ctx)
+
     def lower(self, obj):
         if not isinstance(obj, OptimizeObjective):
             raise Z3Exception("Expecting objective handle returned by maximize/minimize")

src/api/z3_optimization.h

@@ -117,10 +117,12 @@ extern "C" {
        \brief Check consistency and produce optimal values.
        \param c - context
        \param o - optimization context
+       \param num_assumptions - number of additional assumptions
+       \param assumptions - the additional assumptions
 
-       def_API('Z3_optimize_check', INT, (_in(CONTEXT), _in(OPTIMIZE)))
+       def_API('Z3_optimize_check', INT, (_in(CONTEXT), _in(OPTIMIZE), _in(UINT), _in_array(2, AST)))
     */
-    Z3_lbool Z3_API Z3_optimize_check(Z3_context c, Z3_optimize o);
+    Z3_lbool Z3_API Z3_optimize_check(Z3_context c, Z3_optimize o, unsigned num_assumptions, Z3_ast const assumptions[]);
 
 
     /**
@@ -143,6 +145,14 @@ extern "C" {
     */
     Z3_model Z3_API Z3_optimize_get_model(Z3_context c, Z3_optimize o);
 
+    /**
+       \brief Retrieve the unsat core for the last #Z3_optimize_chec
+       The unsat core is a subset of the assumptions \c a.
+
+       def_API('Z3_optimize_get_unsat_core', AST_VECTOR, (_in(CONTEXT), _in(OPTIMIZE)))       
+     */
+    Z3_ast_vector Z3_API Z3_optimize_get_unsat_core(Z3_context c, Z3_optimize o);
+
     /**
        \brief Set parameters on optimization context.
 

src/ast/pattern/expr_pattern_match.cpp

@@ -393,10 +393,8 @@ expr_pattern_match::initialize(char const * spec_string) {
     VERIFY(parse_smt2_commands(ctx, is));
     ctx.set_print_success(ps);
 
-    ptr_vector<expr>::const_iterator it  = ctx.begin_assertions();
+    for (expr * e : ctx.assertions()) {
-    ptr_vector<expr>::const_iterator end = ctx.end_assertions();
+        compile(e);
-    for (; it != end; ++it) {
-        compile(*it);
     }
     TRACE("expr_pattern_match", display(tout); );
 }

src/cmd_context/cmd_context.cpp

@@ -1312,7 +1312,7 @@ void cmd_context::assert_expr(expr * t) {
     m().inc_ref(t);
     m_assertions.push_back(t);
     if (produce_unsat_cores())
-        m_assertion_names.push_back(0);
+        m_assertion_names.push_back(nullptr);
     if (m_solver)
         m_solver->assert_expr(t);
 }
@@ -1488,13 +1488,24 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
         scoped_ctrl_c ctrlc(eh);
         scoped_timer timer(timeout, &eh);
         scoped_rlimit _rlimit(m().limit(), rlimit);
+        expr_ref_vector asms(m());
+        asms.append(num_assumptions, assumptions);
         if (!m_processing_pareto) {
-            ptr_vector<expr> cnstr(m_assertions);
+            expr_ref_vector assertions(m());
-            cnstr.append(num_assumptions, assumptions);
+            unsigned sz = m_assertions.size();
-            get_opt()->set_hard_constraints(cnstr);
+            for (unsigned i = 0; i < sz; ++i) {
+                if (m_assertion_names.size() > i && m_assertion_names[i]) {
+                    asms.push_back(m_assertion_names[i]);
+                    assertions.push_back(m().mk_implies(m_assertion_names[i], m_assertions[i]));
+                }
+                else {
+                    assertions.push_back(m_assertions[i]);
+                }
+            }
+            get_opt()->set_hard_constraints(assertions);
         }
         try {
-            r = get_opt()->optimize();
+            r = get_opt()->optimize(asms);
             if (r == l_true && get_opt()->is_pareto()) {
                 m_processing_pareto = true;
             }
@@ -1802,11 +1813,8 @@ void cmd_context::validate_model() {
         cancel_eh<reslimit> eh(m().limit());
         expr_ref r(m());
         scoped_ctrl_c ctrlc(eh);
-        ptr_vector<expr>::const_iterator it  = begin_assertions();
-        ptr_vector<expr>::const_iterator end = end_assertions();
         bool invalid_model = false;
-        for (; it != end; ++it) {
+        for (expr * a : assertions()) {
-            expr * a = *it;
             if (is_ground(a)) {
                 r = nullptr;
                 evaluator(a, r);

src/cmd_context/cmd_context.h

@@ -148,8 +148,8 @@ public:
     virtual bool empty() = 0;
     virtual void push() = 0;
     virtual void pop(unsigned n) = 0;
-    virtual lbool optimize() = 0;
+    virtual lbool optimize(expr_ref_vector const& asms) = 0;
-    virtual void set_hard_constraints(ptr_vector<expr> & hard) = 0;
+    virtual void set_hard_constraints(expr_ref_vector const & hard) = 0;
     virtual void display_assignment(std::ostream& out) = 0;
     virtual bool is_pareto() = 0;
     virtual void set_logic(symbol const& s) = 0;
@@ -452,11 +452,8 @@ public:
 
     double get_seconds() const { return m_watch.get_seconds(); }
 
-    ptr_vector<expr>::const_iterator begin_assertions() const { return m_assertions.begin(); }
+    ptr_vector<expr> const& assertions() const { return m_assertions; }
-    ptr_vector<expr>::const_iterator end_assertions() const { return m_assertions.end(); }
+    ptr_vector<expr> const& assertion_names() const { return m_assertion_names; }
-
-    ptr_vector<expr>::const_iterator begin_assertion_names() const { return m_assertion_names.begin(); }
-    ptr_vector<expr>::const_iterator end_assertion_names() const { return m_assertion_names.end(); }
 
     /**
        \brief Hack: consume assertions if there are no scopes.

src/cmd_context/cmd_context_to_goal.cpp

@@ -28,20 +28,18 @@ void assert_exprs_from(cmd_context const & ctx, goal & t) {
     ast_manager & m = t.m();
     bool proofs_enabled = t.proofs_enabled();
     if (ctx.produce_unsat_cores()) {
-        ptr_vector<expr>::const_iterator it   = ctx.begin_assertions();
+        ptr_vector<expr>::const_iterator it   = ctx.assertions().begin();
-        ptr_vector<expr>::const_iterator end  = ctx.end_assertions();
+        ptr_vector<expr>::const_iterator end  = ctx.assertions().end();
-        ptr_vector<expr>::const_iterator it2  = ctx.begin_assertion_names();
+        ptr_vector<expr>::const_iterator it2  = ctx.assertion_names().begin();
-        SASSERT(end - it == ctx.end_assertion_names() - it2);
+        SASSERT(ctx.assertions().size() == ctx.assertion_names().size());
         for (; it != end; ++it, ++it2) {
             t.assert_expr(*it, proofs_enabled ? m.mk_asserted(*it) : nullptr, m.mk_leaf(*it2));
         }
     }
     else {
-        ptr_vector<expr>::const_iterator it  = ctx.begin_assertions();
+        for (expr * e : ctx.assertions()) {
-        ptr_vector<expr>::const_iterator end = ctx.end_assertions();
+            t.assert_expr(e, proofs_enabled ? m.mk_asserted(e) : nullptr, nullptr);
-        for (; it != end; ++it) {
-            t.assert_expr(*it, proofs_enabled ? m.mk_asserted(*it) : nullptr, nullptr);
         }
-        SASSERT(ctx.begin_assertion_names() == ctx.end_assertion_names());
+        SASSERT(ctx.assertion_names().empty());
     }
 }

src/muz/fp/dl_cmds.cpp

@@ -332,10 +332,8 @@ public:
 private:
     void set_background(cmd_context& ctx) {
         datalog::context& dlctx = m_dl_ctx->dlctx();
-        ptr_vector<expr>::const_iterator it  = ctx.begin_assertions();
+        for (expr * e : ctx.assertions()) {
-        ptr_vector<expr>::const_iterator end = ctx.end_assertions();
+            dlctx.assert_expr(e);
-        for (; it != end; ++it) {
-            dlctx.assert_expr(*it);
         }
     }
 

src/opt/opt_context.cpp

@@ -79,13 +79,13 @@ namespace opt {
         m_hard.push_back(hard);
     }
 
-    bool context::scoped_state::set(ptr_vector<expr> & hard) {
+    bool context::scoped_state::set(expr_ref_vector const & hard) {
         bool eq = hard.size() == m_hard.size();
         for (unsigned i = 0; eq && i < hard.size(); ++i) {
-            eq = hard[i] == m_hard[i].get();
+            eq = hard.get(i) == m_hard.get(i);
         }
         m_hard.reset();
-        m_hard.append(hard.size(), hard.c_ptr());
+        m_hard.append(hard);
         return !eq;
     }
 
@@ -130,6 +130,7 @@ namespace opt {
         m_fm(alloc(generic_model_converter, m, "opt")),
         m_model_fixed(),
         m_objective_refs(m),
+        m_core(m),
         m_enable_sat(false),
         m_is_clausal(false),
         m_pp_neat(false),
@@ -173,11 +174,10 @@ namespace opt {
     }
 
     void context::get_unsat_core(expr_ref_vector & r) { 
-        throw default_exception("Unsat cores are not supported with optimization"); 
+        r.append(m_core);
     }
 
-
+    void context::set_hard_constraints(expr_ref_vector const& fmls) {
-    void context::set_hard_constraints(ptr_vector<expr>& fmls) {
         if (m_scoped_state.set(fmls)) {
             clear_state();
         }
@@ -253,7 +253,7 @@ namespace opt {
         m_hard_constraints.append(s.m_hard);
     }
 
-    lbool context::optimize() {
+    lbool context::optimize(expr_ref_vector const& asms) {
         if (m_pareto) {
             return execute_pareto();
         }
@@ -263,7 +263,10 @@ namespace opt {
         clear_state();
         init_solver(); 
         import_scoped_state(); 
-        normalize();
+        normalize(asms);
+        if (m_hard_constraints.size() == 1 && m.is_false(m_hard_constraints.get(0))) {
+            return l_false;
+        }
         internalize();
         update_solver();
         if (contains_quantifiers()) {
@@ -281,7 +284,7 @@ namespace opt {
         symbol pri = optp.priority();
 
         IF_VERBOSE(1, verbose_stream() << "(optimize:check-sat)\n");
-        lbool is_sat = s.check_sat(0,nullptr);
+        lbool is_sat = s.check_sat(asms.size(),asms.c_ptr());
         TRACE("opt", s.display(tout << "initial search result: " << is_sat << "\n");); 
         if (is_sat != l_false) {
             s.get_model(m_model);
@@ -289,7 +292,10 @@ namespace opt {
             model_updated(m_model.get());
         }
         if (is_sat != l_true) {
-            TRACE("opt", tout << m_hard_constraints << "\n";);            
+            TRACE("opt", tout << m_hard_constraints << " " << asms << "\n";);            
+            if (!asms.empty()) {
+                s.get_unsat_core(m_core);
+            }
             return is_sat;
         }
         IF_VERBOSE(1, verbose_stream() << "(optimize:sat)\n");
@@ -479,7 +485,6 @@ namespace opt {
         return r;
     }
 
-
     expr_ref context::mk_le(unsigned i, model_ref& mdl) {
         objective const& obj = m_objectives[i];
         return mk_cmp(false, mdl, obj);
@@ -489,8 +494,7 @@ namespace opt {
         objective const& obj = m_objectives[i];
         return mk_cmp(true, mdl, obj);
     }
-    
+        
-    
     expr_ref context::mk_gt(unsigned i, model_ref& mdl) {
         expr_ref result = mk_le(i, mdl);
         result = mk_not(m, result);
@@ -751,22 +755,25 @@ namespace opt {
         return m_arith.is_numeral(e, n) || m_bv.is_numeral(e, n, sz);
     }
 
-    void context::normalize() {
+    void context::normalize(expr_ref_vector const& asms) {
         expr_ref_vector fmls(m);
         to_fmls(fmls);
-        simplify_fmls(fmls);
+        simplify_fmls(fmls, asms);
         from_fmls(fmls);
     }
 
-    void context::simplify_fmls(expr_ref_vector& fmls) {
+    void context::simplify_fmls(expr_ref_vector& fmls, expr_ref_vector const& asms) {
         if (m_is_clausal) {
             return;
         }
 
-        goal_ref g(alloc(goal, m, true, false));
+        goal_ref g(alloc(goal, m, true, !asms.empty()));
         for (expr* fml : fmls) {
             g->assert_expr(fml);
         }
+        for (expr * a : asms) {
+            g->assert_expr(a, a);
+        }
         tactic_ref tac0 = 
             and_then(mk_simplify_tactic(m, m_params), 
                      mk_propagate_values_tactic(m),
@@ -788,6 +795,7 @@ namespace opt {
             set_simplify(tac0.get());
         }
         goal_ref_buffer result;
+        TRACE("opt", g->display(tout););
         (*m_simplify)(g, result); 
         SASSERT(result.size() == 1);
         goal* r = result[0];
@@ -795,8 +803,27 @@ namespace opt {
         fmls.reset();
         expr_ref tmp(m);
         for (unsigned i = 0; i < r->size(); ++i) {
-            fmls.push_back(r->form(i));
+            if (asms.empty()) {
+                fmls.push_back(r->form(i));
+                continue;
+            }
+
+            ptr_vector<expr> deps;
+            expr_dependency_ref core(r->dep(i), m);
+            m.linearize(core, deps);
+            if (!deps.empty()) {
+                fmls.push_back(m.mk_implies(m.mk_and(deps.size(), deps.c_ptr()), r->form(i)));
+            }
+            else {
+                fmls.push_back(r->form(i));
+            }
         }        
+        if (r->inconsistent()) {
+            ptr_vector<expr> core_elems;
+            expr_dependency_ref core(r->dep(0), m);
+            m.linearize(core, core_elems);
+            m_core.append(core_elems.size(), core_elems.c_ptr());
+        }
     }
 
     bool context::is_maximize(expr* fml, app_ref& term, expr_ref& orig_term, unsigned& index) {
@@ -1395,6 +1422,7 @@ namespace opt {
         m_box_index = UINT_MAX;
         m_model.reset();
         m_model_fixed.reset();
+        m_core.reset();
     }
 
     void context::set_pareto(pareto_base* p) {

src/opt/opt_context.h

@@ -133,7 +133,7 @@ namespace opt {
             void push();
             void pop();
             void add(expr* hard);
-            bool set(ptr_vector<expr> & hard);
+            bool set(expr_ref_vector const&  hard);
             unsigned add(expr* soft, rational const& weight, symbol const& id);
             unsigned add(app* obj, bool is_max);
             unsigned get_index(symbol const& id) { return m_indices[id]; }
@@ -164,6 +164,7 @@ namespace opt {
         obj_map<func_decl, unsigned> m_objective_fns;
         obj_map<func_decl, expr*>    m_objective_orig;
         func_decl_ref_vector         m_objective_refs;
+        expr_ref_vector              m_core;
         tactic_ref                   m_simplify;
         bool                         m_enable_sat;
         bool                         m_enable_sls;
@@ -186,8 +187,8 @@ namespace opt {
         void push() override;
         void pop(unsigned n) override;
         bool empty() override { return m_scoped_state.m_objectives.empty(); }
-        void set_hard_constraints(ptr_vector<expr> & hard) override;
+        void set_hard_constraints(expr_ref_vector const& hard) override;
-        lbool optimize() override;
+        lbool optimize(expr_ref_vector const& asms) override;
         void set_model(model_ref& _m) override { m_model = _m; }
         void get_model_core(model_ref& _m) override;
         void get_box_model(model_ref& _m, unsigned index) override;
@@ -254,7 +255,7 @@ namespace opt {
 
         void reset_maxsmts();
         void import_scoped_state();
-        void normalize();
+        void normalize(expr_ref_vector const& asms);
         void internalize();
         bool is_maximize(expr* fml, app_ref& term, expr_ref& orig_term, unsigned& index);
         bool is_minimize(expr* fml, app_ref& term, expr_ref& orig_term, unsigned& index);
@@ -270,7 +271,7 @@ namespace opt {
         expr* mk_objective_fn(unsigned index, objective_t ty, unsigned sz, expr*const* args);
         void to_fmls(expr_ref_vector& fmls);
         void from_fmls(expr_ref_vector const& fmls);
-        void simplify_fmls(expr_ref_vector& fmls);
+        void simplify_fmls(expr_ref_vector& fmls, expr_ref_vector const& asms);
         void mk_atomic(expr_ref_vector& terms);
 
         void update_lower() { update_bound(true); }

src/opt/opt_pareto.cpp

@@ -71,7 +71,7 @@ namespace opt {
         fmls.push_back(mk_or(gt));
         fml = mk_and(fmls);
         IF_VERBOSE(10, verbose_stream() << "dominates: " << fml << "\n";);
-        TRACE("opt", tout << fml << "\n"; model_smt2_pp(tout, m, *m_model, 0););
+        TRACE("opt", model_smt2_pp(tout << fml << "\n", m, *m_model, 0););
         m_solver->assert_expr(fml);        
     }
 

src/parsers/smt2/marshal.cpp

@@ -36,11 +36,12 @@ std::string marshal(expr_ref e, ast_manager &m) {
 expr_ref unmarshal(std::istream &is, ast_manager &m) {
     cmd_context ctx(false, &m);
     ctx.set_ignore_check(true);
-    if (!parse_smt2_commands(ctx, is)) { return expr_ref(nullptr, m); }
+    if (!parse_smt2_commands(ctx, is)) { 
+        return expr_ref(nullptr, m); 
+    }
 
-    ptr_vector<expr>::const_iterator it  = ctx.begin_assertions();
+    ptr_vector<expr>::const_iterator it  = ctx.assertions().begin();
-    ptr_vector<expr>::const_iterator end = ctx.end_assertions();
+    unsigned size = ctx.assertions().size();
-    unsigned size = static_cast<unsigned>(end - it);
     return expr_ref(mk_and(m, size, it), m);
 }
 

src/sat/sat_solver.cpp

@@ -78,6 +78,8 @@ namespace sat {
         del_clauses(m_clauses);
         TRACE("sat", tout << "Delete learned\n";);
         del_clauses(m_learned);
+        dealloc(m_cuber);
+        m_cuber = nullptr;
     }
 
     void solver::del_clauses(clause_vector& clauses) {

src/shell/opt_frontend.cpp

@@ -108,7 +108,8 @@ static unsigned parse_opt(std::istream& in, opt_format f) {
         unsigned rlimit = std::stoi(gparams::get_value("rlimit"));
         scoped_timer timer(timeout, &eh);
         scoped_rlimit _rlimit(m.limit(), rlimit);
-        lbool r = opt.optimize();
+        expr_ref_vector asms(m);
+        lbool r = opt.optimize(asms);
         switch (r) {
         case l_true:  std::cout << "sat\n"; break;
         case l_false: std::cout << "unsat\n"; break;

src/smt/theory_arith_aux.h

@@ -1103,6 +1103,7 @@ namespace smt {
                 e = m_util.mk_gt(obj, e);
             }
         }
+        TRACE("opt", tout << e << "\n";);
         return e;
     }
 
@@ -1119,6 +1120,8 @@ namespace smt {
         std::ostringstream strm;
         strm << val << " <= " << mk_pp(get_enode(v)->get_owner(), get_manager());
         app* b = m.mk_const(symbol(strm.str().c_str()), m.mk_bool_sort());
+        expr_ref result(b, m);
+        TRACE("opt", tout << result << "\n";);
         if (!ctx.b_internalized(b)) {
             fm.hide(b->get_decl());
             bool_var bv = ctx.mk_bool_var(b);
@@ -1133,7 +1136,7 @@ namespace smt {
             TRACE("arith", tout << mk_pp(b, m) << "\n";
                   display_atom(tout, a, false););            
         }
-        return expr_ref(b, m);
+        return result;
     }
 
 

src/smt/theory_lra.cpp

@@ -1412,7 +1412,7 @@ public:
     }
 
     final_check_status final_check_eh() {
-        IF_VERBOSE(2, verbose_stream() << "final-check\n");
+        IF_VERBOSE(2, verbose_stream() << "final-check " << m_solver->get_status() << "\n");
         m_use_nra_model = false;
         lbool is_sat = l_true;
         if (m_solver->get_status() != lp::lp_status::OPTIMAL) {

src/test/arith_rewriter.cpp

@@ -1,4 +1,3 @@
-
 /*++
 Copyright (c) 2015 Microsoft Corporation
 
@@ -26,8 +25,8 @@ static expr_ref parse_fml(ast_manager& m, char const* str) {
            << "(assert " << str << ")\n";
     std::istringstream is(buffer.str());
     VERIFY(parse_smt2_commands(ctx, is));
-    ENSURE(ctx.begin_assertions() != ctx.end_assertions());
+    ENSURE(!ctx.assertions().empty());
-    result = *ctx.begin_assertions();
+    result = ctx.assertions().get(0);
     return result;
 }
 

src/test/polynorm.cpp

@@ -25,8 +25,7 @@ static expr_ref parse_fml(ast_manager& m, char const* str) {
            << "(assert " << str << ")\n";
     std::istringstream is(buffer.str());
     VERIFY(parse_smt2_commands(ctx, is));
-    ENSURE(ctx.begin_assertions() != ctx.end_assertions());
+    result = ctx.assertions().get(0);
-    result = *ctx.begin_assertions();
     return result;
 }
 

src/test/qe_arith.cpp

@@ -37,8 +37,7 @@ static expr_ref parse_fml(ast_manager& m, char const* str) {
            << "(assert " << str << ")\n";
     std::istringstream is(buffer.str());
     VERIFY(parse_smt2_commands(ctx, is));
-    ENSURE(ctx.begin_assertions() != ctx.end_assertions());
+    result = ctx.assertions().get(0);
-    result = *ctx.begin_assertions();
     return result;
 }
 

src/test/quant_solve.cpp

@@ -131,8 +131,7 @@ static expr_ref parse_fml(ast_manager& m, char const* str) {
            << "(assert " << str << ")\n";
     std::istringstream is(buffer.str());
     VERIFY(parse_smt2_commands(ctx, is));
-    ENSURE(ctx.begin_assertions() != ctx.end_assertions());
+    result = ctx.assertions().get(0);
-    result = *ctx.begin_assertions();
     return result;
 }
 

src/util/lp/lar_solver.cpp

@@ -377,7 +377,7 @@ void lar_solver::pop(unsigned k) {
     m_settings.simplex_strategy() = m_simplex_strategy;
     lp_assert(sizes_are_correct());
     lp_assert((!m_settings.use_tableau()) || m_mpq_lar_core_solver.m_r_solver.reduced_costs_are_correct_tableau());
-    m_status = m_mpq_lar_core_solver.m_r_solver.current_x_is_feasible()? lp_status::OPTIMAL: lp_status::UNKNOWN;
+    set_status(lp_status::UNKNOWN);
 }
     
 vector<constraint_index> lar_solver::get_all_constraint_indices() const {

src/util/lp/lar_solver.h

@@ -94,7 +94,6 @@ class lar_solver : public column_namer {
     var_register m_var_register;
     stacked_vector<ul_pair>                             m_columns_to_ul_pairs;
     vector<lar_base_constraint*>                        m_constraints;
-private:
     stacked_value<unsigned>                             m_constraint_count;
     // the set of column indices j such that bounds have changed for j
     int_set                                             m_columns_with_changed_bound;