better recovery from incompleteness and interp failure in duality

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

@@ -562,7 +562,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;