summaryrefslogtreecommitdiff
path: root/src/theory/arith/normal_form.cpp
diff options
context:
space:
mode:
authorTim King <taking@cs.nyu.edu>2012-11-11 00:28:05 +0000
committerTim King <taking@cs.nyu.edu>2012-11-11 00:28:05 +0000
commit341794b1cbd5693010c78b9f5bfe232ee90404b0 (patch)
treeb03c9a0d39050cf0fb5dbfe7393435adc7c5de19 /src/theory/arith/normal_form.cpp
parenta4bebb3ec1e27b433b63dcb2b82f6385e0c40561 (diff)
Fixes for the arithmetic normal form and rewriter to handle arbitrary constants for total functions.
Diffstat (limited to 'src/theory/arith/normal_form.cpp')
-rw-r--r--src/theory/arith/normal_form.cpp6
1 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp
index 9bd0a3b6c..c863bf3c5 100644
--- a/src/theory/arith/normal_form.cpp
+++ b/src/theory/arith/normal_form.cpp
@@ -27,9 +27,9 @@ namespace arith {
bool Variable::isDivMember(Node n){
switch(n.getKind()){
- case kind::DIVISION:
- case kind::INTS_DIVISION:
- case kind::INTS_MODULUS:
+ //case kind::DIVISION:
+ //case kind::INTS_DIVISION:
+ //case kind::INTS_MODULUS:
case kind::DIVISION_TOTAL:
case kind::INTS_DIVISION_TOTAL:
case kind::INTS_MODULUS_TOTAL:
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback