From c9cf658e7ccc19f470789e923e10f84ffa7d54f2 Mon Sep 17 00:00:00 2001
From: Ken McMillan <kenmcmil@microsoft.com>
Date: Wed, 19 Feb 2014 13:56:55 -0800
Subject: [PATCH] interpolation fix for commutativity
---
src/interp/iz3proof_itp.cpp | 10 ++++++++--
1 file changed, 8 insertions(+), 2 deletions(-)
diff --git a/src/interp/iz3proof_itp.cpp b/src/interp/iz3proof_itp.cpp
index cf86e9914..fac7849ec 100755
--- a/src/interp/iz3proof_itp.cpp
+++ b/src/interp/iz3proof_itp.cpp
@@ -2146,8 +2146,14 @@ class iz3proof_itp_impl : public iz3proof_itp {
/** Make a Reflexivity node. This rule produces |- x = x */
virtual node make_reflexivity(ast con){
- throw proof_error();
-}
+ if(get_term_type(con) == LitA)
+ return mk_false();
+ if(get_term_type(con) == LitB)
+ return mk_true();
+ ast itp = make(And,make(contra,no_proof,mk_false()),
+ make(contra,mk_true(),mk_not(con)));
+ return itp;
+ }
/** Make a Symmetry node. This takes a derivation of |- x = y and
produces | y = x. Ditto for ~(x=y) */