From 2a2c5102e10a8b3f1091bc50916fda5e766b5d4a Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Wed, 13 Mar 2013 18:27:11 -0400
Subject: [PATCH] Better error in case of nonlinear assertions while in linear
 logic

---
 src/theory/arith/arith_rewriter.cpp | 4 ++--
 src/theory/arith/normal_form.cpp    | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index 823b61df5..ee9ff9e1b 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -86,7 +86,7 @@ RewriteResponse ArithRewriter::preRewriteTerm(TNode t){
   }else if(t.isVar()){
     return rewriteVariable(t);
   }else{
-    switch(t.getKind()){
+    switch(Kind k = t.getKind()){
     case kind::MINUS:
       return rewriteMinus(t, true);
     case kind::UMINUS:
@@ -104,7 +104,7 @@ RewriteResponse ArithRewriter::preRewriteTerm(TNode t){
     case kind::INTS_MODULUS_TOTAL:
       return rewriteIntsDivModTotal(t,true);
     default:
-      Unreachable();
+      Unhandled(k);
     }
   }
 }
diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp
index fd6f04ca8..9bd0a3b6c 100644
--- a/src/theory/arith/normal_form.cpp
+++ b/src/theory/arith/normal_form.cpp
@@ -28,8 +28,8 @@ namespace arith {
 bool Variable::isDivMember(Node n){
   switch(n.getKind()){
   case kind::DIVISION:
-    //case kind::INTS_DIVISION:
-    //case kind::INTS_MODULUS:
+  case kind::INTS_DIVISION:
+  case kind::INTS_MODULUS:
   case kind::DIVISION_TOTAL:
   case kind::INTS_DIVISION_TOTAL:
   case kind::INTS_MODULUS_TOTAL:
-- 
2.30.2