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

scripts/release.yml

@@ -69,6 +69,10 @@ jobs:
     inputs:
      artifactName: 'Ubuntu'
      targetPath: tmp
+  - task: CopyFiles@2
+    inputs:
+     sourceFolder: $(Build.ArtifactStagingDirectory)
+     targetFolder: tmp
 # TBD: build NuGet package
 # TBD: this script should build a specific pre-specified tag
   - task: GitHubRelease@0

src/smt/theory_recfun.cpp

@@ -88,7 +88,11 @@ namespace smt {
         // the internalization of the arguments may have triggered the internalization of term.
         if (!ctx().e_internalized(term)) {            
             ctx().mk_enode(term, false, false, true);
+            if (!ctx().relevancy() && u().is_defined(term)) {
+                push_case_expand(alloc(case_expansion, u(), term));
+            }
         }
+
         return true; 
     }
 
@@ -117,8 +121,8 @@ namespace smt {
      */
     void theory_recfun::relevant_eh(app * n) {
         SASSERT(ctx().relevancy());
+        TRACEFN("relevant_eh: (defined) " <<  u().is_defined(n) << " " << mk_pp(n, m));        
         if (u().is_defined(n) && u().has_defs()) {
-            TRACEFN("relevant_eh: (defined) " <<  mk_pp(n, m));        
             push_case_expand(alloc(case_expansion, u(), n));
         }
     }

src/tactic/arith/purify_arith_tactic.cpp

@@ -181,6 +181,10 @@ struct purify_arith_proc {
         return true;
     }
   
+    struct div_def {
+        expr* x, *y, *d;
+        div_def(expr* x, expr* y, expr* d): x(x), y(y), d(d) {}
+    };
 
     struct rw_cfg : public default_rewriter_cfg {
         purify_arith_proc &  m_owner;
@@ -189,6 +193,7 @@ struct purify_arith_proc {
         expr_ref_vector      m_pinned;
         expr_ref_vector      m_new_cnstrs;
         proof_ref_vector     m_new_cnstr_prs;
+        svector<div_def>     m_divs;
         expr_ref             m_subst;
         proof_ref            m_subst_pr;
         expr_ref_vector      m_new_vars;
@@ -297,12 +302,13 @@ struct purify_arith_proc {
                           EQ(u().mk_mul(y, k), x)));
             push_cnstr_pr(result_pr);
             rational r;
-            if (complete() && (!u().is_numeral(y, r) || r.is_zero())) {
+            if (complete()) {
                 // y != 0 \/ k = div-0(x)
                 push_cnstr(OR(NOT(EQ(y, mk_real_zero())),
                               EQ(k, u().mk_div(x, mk_real_zero()))));
                 push_cnstr_pr(result_pr);
             }
+            m_divs.push_back(div_def(x, y, k));
         }
    
         void process_idiv(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { 
@@ -768,6 +774,16 @@ struct purify_arith_proc {
         for (unsigned i = 0; i < sz; i++) {
             m_goal.assert_expr(r.cfg().m_new_cnstrs.get(i), m_produce_proofs ? r.cfg().m_new_cnstr_prs.get(i) : nullptr, nullptr);
         }
+        auto const& divs = r.cfg().m_divs;
+        for (unsigned i = 0; i < divs.size(); ++i) {
+            auto const& p1 = divs[i];
+            for (unsigned j = i + 1; j < divs.size(); ++j) {
+                auto const& p2 = divs[j];
+                m_goal.assert_expr(m().mk_implies(
+                                       m().mk_and(m().mk_eq(p1.x, p2.x), m().mk_eq(p1.y, p2.y)), 
+                                       m().mk_eq(p1.d, p2.d)));
+            }
+        }
         
         // add generic_model_converter to eliminate auxiliary variables from model
         if (produce_models) {