diff --git a/src/interp/iz3proof_itp.cpp b/src/interp/iz3proof_itp.cpp
index 52ddcd64f..df436d206 100755
--- a/src/interp/iz3proof_itp.cpp
+++ b/src/interp/iz3proof_itp.cpp
@@ -1027,7 +1027,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
 	linear_comb(Aineqs,coeff,make(Leq,make_int(rational(0)),make(Sub,term2,term1)));
     }
     else {
-      ast pf = extract_rewrites(make(concat,mk_true(),rest),p1);
+      ast pf = extract_rewrites(make(concat,mk_true(),last),p1);
       ast new_normal = fix_normal(term1,term2,pf);
       normals = merge_normal_chains(normals,cons_normal(new_normal,mk_true()), Aproves, Bproves);
     }
diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp
index 26786d57a..f65ec72d4 100755
--- a/src/interp/iz3translate.cpp
+++ b/src/interp/iz3translate.cpp
@@ -1712,11 +1712,17 @@ public:
 	std::cout << "foo!\n";
 
       // no idea why this shows up
-      if(dk == PR_MODUS_PONENS_OEQ)
+      if(dk == PR_MODUS_PONENS_OEQ){
 	if(conc(prem(proof,0)) == con){
 	  res = translate_main(prem(proof,0),expect_clause);
 	  return res;
 	}
+	if(expect_clause && op(con) == Or){ // skolemization does this
+	  Iproof::node clause = translate_main(prem(proof,0),true);
+	  res = RewriteClause(clause,prem(proof,1));
+	  return res;
+	}
+      }
       
 #if 0
       if(1 && dk == PR_TRANSITIVITY && pr(prem(proof,1)) == PR_COMMUTATIVITY){
@@ -1800,7 +1806,9 @@ public:
 	}
 	break;
       }
-      case PR_MONOTONICITY: {
+      case PR_QUANT_INTRO:
+      case PR_MONOTONICITY:
+	{
 	std::vector<ast> eqs; eqs.resize(args.size());
 	for(unsigned i = 0; i < args.size(); i++)
 	  eqs[i] = conc(prem(proof,i));