diff --git a/src/interp/iz3mgr.h b/src/interp/iz3mgr.h
index 4ef594cee..3ec2c42d1 100755
--- a/src/interp/iz3mgr.h
+++ b/src/interp/iz3mgr.h
@@ -387,10 +387,13 @@ class iz3mgr  {
     return UnknownTheory;
   }
 
-  enum lemma_kind {FarkasKind,Leq2EqKind,Eq2LeqKind,GCDTestKind,AssignBoundsKind,EqPropagateKind,UnknownKind};
+  enum lemma_kind {FarkasKind,Leq2EqKind,Eq2LeqKind,GCDTestKind,AssignBoundsKind,EqPropagateKind,ArithMysteryKind,UnknownKind};
 
   lemma_kind get_theory_lemma_kind(const ast &proof){
     symb s = sym(proof);
+    if(s->get_num_parameters() < 2) {
+      return ArithMysteryKind;  // Bad -- Z3 hasn't told us
+    }
     ::symbol p0;
     bool ok = s->get_parameter(1).is_symbol(p0);
     if(!ok) return UnknownKind;
diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp
index 5aafa94f7..e467da1fc 100755
--- a/src/interp/iz3translate.cpp
+++ b/src/interp/iz3translate.cpp
@@ -1581,6 +1581,12 @@ public:
     return res;
   }
 
+  ast ArithMysteryRule(const ast &con, const std::vector<ast> &prems, const std::vector<Iproof::node> &args){
+    // Hope for the best!
+    Iproof::node guess = reconstruct_farkas(prems,args,con);
+    return guess;
+  }
+
   struct CannotCombineEqPropagate {};
 
   void CombineEqPropagateRec(const ast &proof, std::vector<ast> &prems, std::vector<Iproof::node> &args, ast &eqprem){
@@ -1892,6 +1898,14 @@ public:
 	    res = EqPropagate(con,prems,args);
 	    break;
 	  }
+	  case ArithMysteryKind: {
+	    // Z3 hasn't told us what kind of lemma this is -- maybe we can guess
+	    std::vector<ast> prems(nprems);
+	    for(unsigned i = 0; i < nprems; i++)
+	      prems[i] = prem(proof,i);
+	    res = ArithMysteryRule(con,prems,args);
+	    break;
+	  }
 	  default:
 	    throw unsupported();
 	  }