From ccc1f0221663c1a67b0d7aa62155b61d6df58020 Mon Sep 17 00:00:00 2001
From: Ken McMillan <kenmcmil@microsoft.com>
Date: Tue, 19 May 2015 18:47:13 -0700
Subject: [PATCH] fix for github issue 54

---
 src/interp/iz3mgr.h         |  6 ++++++
 src/interp/iz3proof_itp.cpp |  8 ++++++--
 src/interp/iz3translate.cpp | 14 +++++++++++++-
 3 files changed, 25 insertions(+), 3 deletions(-)

diff --git a/src/interp/iz3mgr.h b/src/interp/iz3mgr.h
index 3f4138354..54fb35a0f 100755
--- a/src/interp/iz3mgr.h
+++ b/src/interp/iz3mgr.h
@@ -279,6 +279,12 @@ class iz3mgr  {
             res[i] = arg(t,i);
     }
 
+    std::vector<ast> args(const ast &t){
+        std::vector<ast> res;
+        get_args(t,res);
+        return res;
+    }
+
     symb sym(ast t){
         raw_ast *_ast = t.raw();
         return is_app(_ast) ? to_app(_ast)->get_decl() : 0;
diff --git a/src/interp/iz3proof_itp.cpp b/src/interp/iz3proof_itp.cpp
index f76de14cf..2b4100e5e 100755
--- a/src/interp/iz3proof_itp.cpp
+++ b/src/interp/iz3proof_itp.cpp
@@ -2215,8 +2215,12 @@ class iz3proof_itp_impl : public iz3proof_itp {
         }
         else {
             if(get_term_type(p) == LitA){
-                if(get_term_type(q) == LitA)
-                    itp = mk_false();
+                if(get_term_type(q) == LitA){
+                    if(op(q) == Or)
+                        itp = make_assumption(rng.hi,args(q));
+                    else 
+                        itp = mk_false();
+                }
                 else {
                     if(get_term_type(p_eq_q) == LitA)
                         itp = q;
diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp
index e4bccace1..d1479e4cc 100755
--- a/src/interp/iz3translate.cpp
+++ b/src/interp/iz3translate.cpp
@@ -1702,14 +1702,16 @@ public:
                     return res;
                 }
             }
-            if(dk == PR_MODUS_PONENS && expect_clause && op(con) == Or){
+            if(dk == PR_MODUS_PONENS && expect_clause && op(con) == Or && op(conc(prem(proof,0))) == Or){
                 Iproof::node clause = translate_main(prem(proof,0),true);
                 res = RewriteClause(clause,prem(proof,1));
                 return res;
             }
 
+#if 0
             if(dk == PR_MODUS_PONENS && expect_clause && op(con) == Or)
                 std::cout << "foo!\n";
+#endif
 
             // no idea why this shows up
             if(dk == PR_MODUS_PONENS_OEQ){
@@ -1965,6 +1967,16 @@ public:
                 res = make(commute,pf,comm_equiv);
                 break;
             }
+            case PR_AND_ELIM: {
+                std::vector<ast> rule_ax, res_conc;
+                ast piv = conc(prem(proof,0));
+                rule_ax.push_back(make(Not,piv));
+                rule_ax.push_back(con);
+                ast pf = iproof->make_axiom(rule_ax);
+                res_conc.push_back(con);
+                res = iproof->make_resolution(piv,res_conc,pf,args[0]);
+                break;
+            }
             default:
                 pfgoto(proof);
                 assert(0 && "translate_main: unsupported proof rule");