10 files changed, 42 insertions, 8 deletions
diff --git a/src/expr/builtin_type_rules.h b/src/expr/builtin_type_rules.h
index 2a6b43b22..e0ad0b038 100644
--- a/src/expr/builtin_type_rules.h
+++ b/src/expr/builtin_type_rules.h
@@ -23,7 +23,7 @@ namespace CVC4 {
 
 class EqualityTypeRule {
   public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n) throw (TypeCheckingException) {
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n) throw (TypeCheckingExceptionPrivate) {
     if (n[0].getType() != n[1].getType()) {
       throw TypeCheckingExceptionPrivate(n, "Left and right hand side of the equation are not of the same type");
     }
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index da16000ce..821349b45 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -28,7 +28,8 @@ bool TypeNode::isInteger() const {
 }
 
 bool TypeNode::isReal() const {
-  return getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == REAL_TYPE;
+  return getKind() == kind::TYPE_CONSTANT
+    && (getConst<TypeConstant>() == REAL_TYPE || getConst<TypeConstant>() == INTEGER_TYPE);
 }
 
 /** Is this a function type? */
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 1d32fffda..f7b1a6b9e 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -110,7 +110,7 @@ public:
    * @return true if expressions are equal, false otherwise
    */
   bool operator==(const TypeNode& typeNode) const {
-    return d_nv == typeNode.d_nv;
+    return d_nv == typeNode.d_nv || (typeNode.isReal() && this->isReal());
   }
 
   /**
@@ -119,7 +119,7 @@ public:
    * @return true if expressions are equal, false otherwise
    */
   bool operator!=(const TypeNode& typeNode) const {
-    return d_nv != typeNode.d_nv;
+    return !(*this == typeNode);
   }
 
   /**
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index eb77b0d54..31afa986c 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -338,6 +338,7 @@ Node TseitinCnfStream::handleNonAtomicNode(TNode node) {
 
   if(node.getKind() == ITE) {
     Assert( node.getNumChildren() == 3 );
+    //TODO should this be a skolem?
     Node skolem = nodeManager->mkVar(node.getType());
     Node newAssertion =
         nodeManager->mkNode(
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index 13ee9183f..6f1df5958 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -417,6 +417,9 @@ Node ArithRewriter::rewriteTerm(TNode t){
     return rewritePlus(t);
   }else if(t.getKind() == kind::DIVISION){
     return rewriteConstantDiv(t);
+  }else if(t.getKind() == kind::MINUS){
+    Node sub = makeSubtractionNode(t[0],t[1]);
+    return rewrite(sub);
   }else{
     Unreachable();
     return Node::null();
diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h
index 5d94d20a9..184844dbc 100644
--- a/src/theory/arith/arith_rewriter.h
+++ b/src/theory/arith/arith_rewriter.h
@@ -75,6 +75,7 @@ private:
   Node rewriteTerm(TNode t);
   Node rewriteMult(TNode t);
   Node rewritePlus(TNode t);
+  Node rewriteMinus(TNode t);
   Node makeSubtractionNode(TNode l, TNode r);
 
 
diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h
index 2ab94c195..7237c3a54 100644
--- a/src/theory/arith/tableau.h
+++ b/src/theory/arith/tableau.h
@@ -94,7 +94,7 @@ public:
   void subsitute(Row& row_s){
     TNode x_s = row_s.basicVar();
 
-    Assert(!has(x_s));
+    Assert(has(x_s));
     Assert(x_s != d_x_i);
 
 
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 66883161e..6ca447ea5 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -99,6 +99,7 @@ void TheoryArith::registerTerm(TNode tn){
   if(tn.getKind() == kind::BUILTIN) return;
 
   if(tn.getMetaKind() == metakind::VARIABLE){
+
     setupVariable(tn);
   }
 
@@ -419,12 +420,25 @@ Node TheoryArith::generateConflictBelow(TNode conflictVar){
 Node TheoryArith::simulatePreprocessing(TNode n){
   if(n.getKind() == NOT){
     Node sub = simulatePreprocessing(n[0]);
-    return NodeManager::currentNM()->mkNode(NOT,sub);
+    if(sub.getKind() == NOT){
+      return sub[0];
+    }else{
+      return NodeManager::currentNM()->mkNode(NOT,sub);
+    }
   }else{
     Node rewritten = rewrite(n);
     Kind k = rewritten.getKind();
-    if(!isRelationOperator(k)){
-      return rewritten;
+    bool negate = false;
+
+    if(rewritten.getKind() == NOT){
+      Node sub = simulatePreprocessing(rewritten[0]);
+      if(sub.getKind() == NOT){
+        return sub[0];
+      }else{
+        return NodeManager::currentNM()->mkNode(NOT,sub);
+      }
+    } else if(!isRelationOperator(k)){
+      Unreachable("Slack must be have been created!");
     }else if(rewritten[0].getMetaKind() == metakind::VARIABLE){
       return rewritten;
     }else {
diff --git a/test/regress/regress0/ite_arith.smt2 b/test/regress/regress0/ite_arith.smt2
new file mode 100644
index 000000000..0e171666f
--- /dev/null
+++ b/test/regress/regress0/ite_arith.smt2
@@ -0,0 +1,6 @@
+(set-logic QF_LRA)
+(set-info :status unsat)
+(declare-fun x () Real)
+(declare-fun y () Real)
+(assert (not (= x (ite true x y))))
+(check-sat)
diff --git a/test/regress/regress0/ite_real_int_type.smt b/test/regress/regress0/ite_real_int_type.smt
new file mode 100644
index 000000000..5141a0b42
--- /dev/null
+++ b/test/regress/regress0/ite_real_int_type.smt
@@ -0,0 +1,8 @@
+(benchmark ite_real_int_type
+:logic QF_LRA
+:status sat
+:extrafuns ((x Real))
+:extrafuns ((y Real))
+:formula
+  (and (= 0 (ite true x 1)) (= 0 (ite (= x 0) 0 1)) (= x  (ite true y 0)) (= 0 (ite true 0 0)) )
+)