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

scripts/mk_util.py

@@ -98,7 +98,6 @@ JS_ENABLED=False
 PYTHON_INSTALL_ENABLED=False
 STATIC_LIB=False
 STATIC_BIN=False
-ADD_CHECKSUM=True
 VER_MAJOR=None
 VER_MINOR=None
 VER_BUILD=None
@@ -2442,8 +2441,6 @@ def mk_config():
             static_opt = '/MT'
         else:
             static_opt = '/MD'
-        if ADD_CHECKSUM:
-            extra_opt = ' %s /RELEASE' % extra_opt
         maybe_disable_dynamic_base = '/DYNAMICBASE' if ALWAYS_DYNAMIC_BASE else '/DYNAMICBASE:NO'
         if DEBUG_MODE:
             static_opt = static_opt + 'd'

scripts/release.yml

@@ -71,14 +71,6 @@ jobs:
      targetPath: tmp
 # TBD: build NuGet package
 # TBD: this script should build a specific pre-specified tag
-  - task: GitHubRelease@0
-    inputs:
-      gitHubConnection: Z3GitHub
-      repositoryName: 'Z3Prover/z3'
-      action: 'delete'
-      target: '$(Build.SourceVersion)'
-      tagSource: 'manual'
-      tag: 'Nightly'
   - task: GitHubRelease@0
     inputs:
       gitHubConnection: Z3GitHub
@@ -86,12 +78,12 @@ jobs:
       action: 'create'
       target: '$(Build.SourceVersion)'
       tagSource: 'manual'
-      tag: 'Nightly'
+      tag: 'z3-4.8.6'
-      title: 'Nightly'
+      title: 'z3-4.8.6'
       releaseNotesSource: 'input'
-      releaseNotes: 'nightly build'
+      releaseNotes: '4.8.6 release'
       assets: 'tmp/*'
-      isDraft: false
+      isDraft: true
       isPreRelease: true
 
 

src/ast/proofs/proof_utils.h

@@ -107,6 +107,7 @@ public:
     {
         ast_manager &m = args.get_manager();
         bool_rewriter brwr(m);
+        brwr.set_flat(false);
 
         if (m.is_or(decl))
         { mk_or_core(args, res); }

src/ast/rewriter/arith_rewriter.cpp

@@ -456,6 +456,32 @@ br_status arith_rewriter::mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kin
             st = BR_DONE;
         }
     }
+    expr* e1 = nullptr, *e2 = nullptr;
+    if (m_util.is_div(arg1, e1, e2) && (!is_numeral(e2, a2) || !a2.is_zero())) {
+        new_arg1 = e1;
+        new_arg2 = m_util.mk_mul(e2, arg2);
+        expr_ref zero(m_util.mk_numeral(rational(0), m_util.is_int(arg1)), m());
+        expr_ref is_zero(m().mk_eq(zero, e2), m());
+        expr_ref div0(m_util.mk_div(e1, zero), m());
+        expr_ref mul2(m_util.mk_mul(e2, arg2), m());
+        switch (kind) {
+        case LE: 
+            result = m().mk_or(
+                m().mk_and(is_zero, m_util.mk_le(div0, arg2)),
+                m().mk_and(m_util.mk_gt(e2, zero), m_util.mk_le(e1, mul2)),
+                m().mk_and(m_util.mk_lt(e2, zero), m_util.mk_ge(e1, mul2)));
+            return BR_REWRITE2;
+        case GE: 
+            result = m().mk_or(
+                m().mk_and(is_zero, m_util.mk_ge(div0, arg2)),
+                m().mk_and(m_util.mk_gt(e2, zero), m_util.mk_ge(e1, mul2)),
+                m().mk_and(m_util.mk_lt(e2, zero), m_util.mk_le(e1, mul2)));
+            return BR_REWRITE2;
+        case EQ: 
+            result = m().mk_ite(is_zero, m().mk_eq(div0, arg2), m().mk_eq(e1, mul2));
+            return BR_REWRITE2;
+        }        
+    }
     if ((m_arith_lhs || m_arith_ineq_lhs) && is_numeral(arg2, a2) && is_neg_poly(arg1, new_arg1)) {
         a2.neg();
         new_arg2 = m_util.mk_numeral(a2, m_util.is_int(new_arg1));

src/tactic/smtlogics/qflia_tactic.cpp

@@ -184,7 +184,7 @@ tactic * mk_preamble_tactic(ast_manager& m) {
     pull_ite_p.set_bool("push_ite_arith", false);
     pull_ite_p.set_bool("local_ctx", true);
     pull_ite_p.set_uint("local_ctx_limit", 10000000);
-
+    pull_ite_p.set_bool("hoist_ite", true);
 
     params_ref ctx_simp_p;
     ctx_simp_p.set_uint("max_depth", 30);