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

src/duality/duality.h

@@ -782,6 +782,9 @@ namespace Duality {
         struct ReallyBad {
         };
 
+        // throw when greedy reduction fails
+        struct greedy_reduce_failed {};
+
         /** Pop a scope (see Push). Note, you cannot pop axioms. */
       
         void Pop(int num_scopes);

src/duality/duality_rpfp.cpp

@@ -2870,10 +2870,10 @@ namespace Duality {
             lits = assumps; 
             std::copy(core.begin(),core.end(),std::inserter(lits,lits.end()));
       
-            for(int k = 0; k < 100; k++) // keep trying, maybe MBQI will do something!
+            for(int k = 0; k < 4; k++) // keep trying, maybe MBQI will do something!
                 if((res = CheckCore(lits,full_core)) == unsat)
                     goto is_unsat;
-            throw "should be unsat";
+            throw greedy_reduce_failed();
         }
     is_unsat:
         FilterCore(core,full_core);
@@ -3084,8 +3084,18 @@ namespace Duality {
                     }
                 }
                 // AddToProofCore(*core);
-                SolveSingleNode(root,node);
+                
-
+                try {
+                    SolveSingleNode(root,node);
+                }
+                catch (char const *msg){
+                    // This happens if interpolation fails
+                    Pop(1);
+                    is.pop(1);
+                    delete core;
+                    timer_stop("InterpolateByCases");
+                    throw msg;
+                }
                 {
                     expr itp = GetAnnotation(node);
                     dualModel = is.get_model(); // TODO: what does this mean?

src/duality/duality_solver.cpp

@@ -2295,6 +2295,10 @@ namespace Duality {
                                         reporter->Message(std::string("interpolation failure:") + msg);
                                         throw DoRestart();
                                     }
+                                    catch(const RPFP::greedy_reduce_failed &){
+                                        // if we couldn't reduce, just continue (maybe should restart?)
+                                        reporter->Message("interpolant verification failed");
+                                    }
                                     if(RecordUpdate(node)){
                                         update_count++;
                                         total_updates++;

src/interp/iz3proof_itp.cpp

@@ -564,7 +564,10 @@ class iz3proof_itp_impl : public iz3proof_itp {
                 else res = clone(e,args);
             }
             catch (const cannot_simplify &){
-                res = clone(e,args);
+                if(g == sum)
+                    res = clone(e,args);
+                else
+                    throw "interpolation failure";
             }
         }
         return res;

src/interp/iz3translate.cpp

@@ -1201,9 +1201,12 @@ public:
         ast t = arg(my_con,0);
         ast c = arg(my_con,1);
         ast d = gcd_of_coefficients(t);
+        /*
         t = z3_simplify(mk_idiv(t,d));
         c = z3_simplify(mk_idiv(c,d));
         ast cut_con = make(op(my_con),t,c);
+        */
+        ast cut_con = con;
         return iproof->make_cut_rule(my_con,d,cut_con,res);
     }
 

src/smt/theory_arith_aux.h

@@ -1451,6 +1451,11 @@ namespace smt {
             normalize_gain(min_gain.get_rational(), max_gain);
         }
 
+        if (is_int(x_i) && !max_gain.is_rational()) {
+            max_gain = inf_numeral(floor(max_gain));
+            normalize_gain(min_gain.get_rational(), max_gain);
+        }
+
         if (!max_inc.is_minus_one()) {
             if (is_int(x_i)) {
                 TRACE("opt",
@@ -1597,6 +1602,7 @@ namespace smt {
 
             TRACE("opt", tout << "after traversing row:\nx_i: v" << x_i << ", x_j: v" << x_j << ", gain: " << max_gain << "\n";
                   tout << "best efforts: " << best_efforts << " has shared: " << has_shared << "\n";);
+
             
             if (!has_bound && x_i == null_theory_var && x_j == null_theory_var) {
                 has_shared = false;