diff --git a/src/ast/ast_pp.h b/src/ast/ast_pp.h
index 58ee3145c1a..1b3ca4a8188 100644
--- a/src/ast/ast_pp.h
+++ b/src/ast/ast_pp.h
@@ -31,6 +31,7 @@ struct mk_pp : public mk_ismt2_pp {
     }
 };
 
+
 //<! print vector of ASTs
 class mk_pp_vec {
     ast_manager &   m;
@@ -54,3 +55,16 @@ inline std::ostream& operator<<(std::ostream & out, mk_pp_vec const & pp) {
 }
 
 
+inline std::string operator+(char const* s, mk_pp const& pp) {
+    std::ostringstream strm;
+    strm << s << pp;
+    return strm.str();
+}
+
+inline std::string operator+(std::string const& s, mk_pp const& pp) {
+    std::ostringstream strm;
+    strm << s << pp;
+    return strm.str();
+}
+
+
diff --git a/src/sat/sat_drat.cpp b/src/sat/sat_drat.cpp
index f0ca7132f7c..6d8c4d4774d 100644
--- a/src/sat/sat_drat.cpp
+++ b/src/sat/sat_drat.cpp
@@ -91,7 +91,6 @@ namespace sat {
 
         unsigned len = 0;
 
-
         if (st.is_deleted()) {
             buffer[len++] = 'd';
             buffer[len++] = ' ';
diff --git a/src/sat/smt/euf_proof.cpp b/src/sat/smt/euf_proof.cpp
index 610027c5346..9335e283f4f 100644
--- a/src/sat/smt/euf_proof.cpp
+++ b/src/sat/smt/euf_proof.cpp
@@ -33,31 +33,23 @@ namespace euf {
             drat_log_decl(a->get_decl());
             std::stringstream strm;
             strm << mk_ismt2_func(a->get_decl(), m);
-            if (a->get_num_parameters() == 0)
-                get_drat().def_begin('e', e->get_id(), strm.str());
-            else {
-                get_drat().def_begin('e', e->get_id(), strm.str());
-            }
+            get_drat().def_begin('e', e->get_id(), strm.str());
             for (expr* arg : *a)
                 get_drat().def_add_arg(arg->get_id());
             get_drat().def_end();
         }
         else if (is_var(e)) {
             var* v = to_var(e);
-            std::stringstream strm;
-            strm << mk_pp(e->get_sort(), m);
-            get_drat().def_begin('v', v->get_id(), strm.str());
+            get_drat().def_begin('v', v->get_id(), "" + mk_pp(e->get_sort(), m));
             get_drat().def_add_arg(v->get_idx());
             get_drat().def_end();
         }
         else if (is_quantifier(e)) {
             quantifier* q = to_quantifier(e);
-            std::stringstream strm;
-            strm << "(";
-            strm << (is_forall(q) ? "forall" : (is_exists(q) ? "exists" : "lambda"));
-            for (unsigned i = 0; i < q->get_num_decls(); ++i) {
-                strm << " (" << q->get_decl_name(i) << " " << mk_pp(q->get_decl_sort(i), m) << ")";
-            }
+            std::stringstream strm;           
+            strm << "(" << (is_forall(q) ? "forall" : (is_exists(q) ? "exists" : "lambda"));
+            for (unsigned i = 0; i < q->get_num_decls(); ++i) 
+                strm << " (" << q->get_decl_name(i) << " " << mk_pp(q->get_decl_sort(i), m) << ")";            
             strm << ")";
             get_drat().def_begin('q', q->get_id(), strm.str());
             get_drat().def_add_arg(q->get_expr()->get_id());
@@ -88,7 +80,8 @@ namespace euf {
             }                
             if (m_drat_todo.size() != sz)
                 continue;
-            drat_log_expr1(e);
+            if (!m_drat_asts.contains(e))
+                drat_log_expr1(e);
             m_drat_todo.pop_back();                   
         }
     }
diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
index b4543867543..bdc1b8b9e50 100644
--- a/src/sat/tactic/goal2sat.cpp
+++ b/src/sat/tactic/goal2sat.cpp
@@ -599,8 +599,8 @@ struct goal2sat::imp : public sat::sat_internalizer {
     }
 
     void convert_iff(app * t, bool root, bool sign) {
-        if (t->get_num_args() != 2)
-            throw default_exception("unexpected number of arguments to xor");
+        if (t->get_num_args() != 2)            
+            throw default_exception("unexpected number of arguments to " + mk_pp(t, m));
         SASSERT(t->get_num_args() == 2);
         unsigned sz = m_result_stack.size();
         SASSERT(sz >= 2);
@@ -608,6 +608,8 @@ struct goal2sat::imp : public sat::sat_internalizer {
         sat::literal  l2 = m_result_stack[sz-2];
         m_result_stack.shrink(sz - 2);
         if (root) {
+            if (m.is_xor(t))
+                sign = !sign;
             SASSERT(sz == 2);
             if (sign) {
                 mk_root_clause(l1, l2);
@@ -616,17 +618,20 @@ struct goal2sat::imp : public sat::sat_internalizer {
             else {
                 mk_root_clause(l1, ~l2);
                 mk_root_clause(~l1, l2);
-            }            
+            }                  
         }
         else {
             sat::bool_var k = add_var(false, t);
             sat::literal  l(k, false);
+            if (m.is_xor(t))
+                l1.neg();
             mk_clause(~l, l1, ~l2);
             mk_clause(~l, ~l1, l2);
-            mk_clause(l,  l1, l2);
+            mk_clause(l, l1, l2);
             mk_clause(l, ~l1, ~l2);
-            if (aig()) aig()->add_iff(l, l1, l2);            
-            cache(t, m.is_xor(t) ? ~l : l);
+            if (aig()) aig()->add_iff(l, l1, l2);
+
+            cache(t, l);
             if (sign)
                 l.neg();
             m_result_stack.push_back(l);
@@ -720,7 +725,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
                 convert_iff(t, root, sign);
                 break;
             case OP_XOR:
-                convert_iff(t, root, !sign);
+                convert_iff(t, root, sign);
                 break;
             case OP_IMPLIES:
                 convert_implies(t, root, sign);
@@ -828,6 +833,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
         process(n, false, redundant);
         SASSERT(m_result_stack.size() == sz + 1);
         sat::literal result = m_result_stack.back();
+        TRACE("goal2sat", tout << "done internalize " << result << " " << mk_bounded_pp(n, m, 2) << "\n";);
         m_result_stack.pop_back();
         if (!result.sign() && m_map.to_bool_var(n) == sat::null_bool_var) {
             force_push();
diff --git a/src/shell/drat_frontend.cpp b/src/shell/drat_frontend.cpp
index 647b2844502..f1ae29586d4 100644
--- a/src/shell/drat_frontend.cpp
+++ b/src/shell/drat_frontend.cpp
@@ -122,12 +122,17 @@ class smt_checker {
             m_input_solver->assert_expr(lit2expr(~lit));
         lbool is_sat = m_input_solver->check_sat();
         if (is_sat != l_false) {
-            std::cout << "did not verify: " << lits << "\n";
-            for (sat::literal lit : lits) {
-                std::cout << lit2expr(lit) << "\n";
-            }
+            std::cout << "did not verify: " << is_sat << " " << lits << "\n";
+            for (sat::literal lit : lits) 
+                std::cout << lit2expr(lit) << "\n";            
             std::cout << "\n";
             m_input_solver->display(std::cout);
+            if (is_sat == l_true) {
+                model_ref mdl;
+                m_input_solver->get_model(mdl);
+                std::cout << *mdl << "\n";
+            }
+                
             exit(0);
         }
         m_input_solver->pop(1);