fail gracefully on interpolation errors

src/cmd_context/interpolant_cmds.cpp

@@ -206,17 +206,13 @@ static expr *make_tree(cmd_context & ctx, const ptr_vector<expr> &exprs){
 }
 
 static void get_interpolant(cmd_context & ctx, const ptr_vector<expr> &exprs, params_ref &m_params) {
-    expr *foo = make_tree(ctx,exprs);
+    expr_ref foo(make_tree(ctx, exprs),ctx.m());
-    ctx.m().inc_ref(foo);
+    get_interpolant(ctx,foo.get(),m_params);
-    get_interpolant(ctx,foo,m_params);
-    ctx.m().dec_ref(foo);
 }
 
 static void compute_interpolant(cmd_context & ctx, const ptr_vector<expr> &exprs, params_ref &m_params) {
-    expr *foo = make_tree(ctx, exprs);
+    expr_ref foo(make_tree(ctx, exprs),ctx.m());
-    ctx.m().inc_ref(foo);
+    compute_interpolant_and_maybe_check(ctx,foo.get(),m_params,false);
-    compute_interpolant_and_maybe_check(ctx,foo,m_params,false);
-    ctx.m().dec_ref(foo);
 }
 
 

src/duality/duality_wrapper.cpp

@@ -562,7 +562,14 @@ namespace Duality {
                 opts.set("weak","1"); 
       
             ::ast *proof = m_solver->get_proof();
-            iz3interpolate(m(),proof,_assumptions,_parents,_interpolants,_theory,&opts);
+            try {
+                iz3interpolate(m(),proof,_assumptions,_parents,_interpolants,_theory,&opts);
+            }
+            // If there's an interpolation bug, throw a char *
+            // exception so duality can catch it and restart. 
+            catch (const interpolation_failure &f) {
+                throw f.msg();
+            }
       
             std::vector<expr> linearized_interpolants(_interpolants.size());
             for(unsigned i = 0; i < _interpolants.size(); i++)

src/interp/iz3interp.cpp

@@ -271,7 +271,18 @@ public:
 
         // translate into an interpolatable proof
         profiling::timer_start("Proof translation");
-        tr->translate(proof,pf);
+        try {
+            tr->translate(proof,pf);
+        }
+        catch (const char *msg) {
+            throw interpolation_failure(msg);
+        }
+        catch (const iz3translation::unsupported &) {
+            throw interpolation_error();
+        }
+        catch (const iz3proof::proof_error &) {
+            throw interpolation_error();
+        }
         profiling::timer_stop("Proof translation");
     
         // translate the proof into interpolants
@@ -309,7 +320,18 @@ public:
       
             // translate into an interpolatable proof
             profiling::timer_start("Proof translation");
-            tr->translate(proof,pf);
+            try {
+                tr->translate(proof,pf);
+            }
+            catch (const char *msg) {
+                throw interpolation_failure(msg);
+            }
+            catch (const iz3translation::unsupported &) {
+                throw interpolation_error();
+            }
+            catch (const iz3proof::proof_error &) {
+                throw interpolation_error();
+            }
             profiling::timer_stop("Proof translation");
       
             // translate the proof into interpolants

src/interp/iz3interp.h

@@ -43,6 +43,27 @@ struct iz3_bad_tree {
 struct iz3_incompleteness {
 };
 
+// This is thrown if there is some bug in the
+// interpolation procedure
+class interpolation_failure : public default_exception {
+ public:
+ interpolation_failure(const char *msg)
+     : default_exception(msg)
+    {
+    }
+};
+
+// This is thrown if we cannot derive an interpolant from a proof
+// because it contains unsupported theories or if the proof contains
+// errors
+class interpolation_error : public default_exception {
+ public:
+ interpolation_error()
+     : default_exception("theory not supported by interpolation or bad proof" )
+        {
+        }
+};
+
 typedef interpolation_options_struct *interpolation_options;
 
 /* Compute an interpolant from a proof. This version uses the parents vector

src/interp/iz3translate.cpp

@@ -2041,11 +2041,23 @@ public:
             locality.clear();
 #endif
             iproof = iz3proof_itp::create(this,range_downward(i),weak_mode());
-            Iproof::node ipf = translate_main(proof);
+            try {
-            ast itp = iproof->interpolate(ipf);
+                Iproof::node ipf = translate_main(proof);
-            itps.push_back(itp);
+                ast itp = iproof->interpolate(ipf);
-            delete iproof;
+                itps.push_back(itp);
-            clear_translation();
+                delete iproof;
+                clear_translation();
+            }
+            catch (const iz3proof_itp::proof_error &) {
+                delete iproof;
+                clear_translation();
+                throw iz3proof::proof_error();
+            }
+            catch (const unsupported &exc) {
+                delete iproof;
+                clear_translation();
+                throw exc;
+            }
         }
         // Very simple proof -- lemma of the empty clause with computed interpolation
         iz3proof::node Ipf = dst.make_lemma(std::vector<ast>(),itps);  // builds result in dst