From: Dejan Jovanović <dejan@cs.nyu.edu>
Date: Fri, 7 Jun 2013 02:55:24 +0000 (-0400)
Subject: small parese issue in IDL
X-Git-Tag: cvc5-1.0.0~7287^2~105
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6a329424666b4c4a6869dd7bcf9e7cfd69a219f5;p=cvc5.git

small parese issue in IDL
---

diff --git a/src/theory/idl/idl_assertion.cpp b/src/theory/idl/idl_assertion.cpp
index c84989d4f..861dd0a46 100644
--- a/src/theory/idl/idl_assertion.cpp
+++ b/src/theory/idl/idl_assertion.cpp
@@ -106,7 +106,7 @@ bool IDLAssertion::parse(TNode node, int c, bool negated) {
     // We parse the negation
     ok = parse(node[0], c, true);
     // Setup the kind
-    if(ok) {
+    if (ok) {
       d_op = negateOp(d_op);
     }
     break;
@@ -119,7 +119,7 @@ bool IDLAssertion::parse(TNode node, int c, bool negated) {
     // All relation operators are parsed on both sides
     d_op = node.getKind();
     ok = parse(node[0], c, negated);
-    if(ok) {
+    if (ok) {
       ok = parse(node[1],-c, negated);
     }
     break;
@@ -137,10 +137,10 @@ bool IDLAssertion::parse(TNode node, int c, bool negated) {
   }
   case kind::MULT: {
     // Only unit multiplication of variables
-    if(node.getNumChildren() == 2 && node[0].isConst()) {
+    if (node.getNumChildren() == 2 && node[0].isConst()) {
       Rational a = node[0].getConst<Rational>();
-      if(a == 1 || a == -1) {
-        return parse(node[1], c * a.sgn(), negated);
+      if (a == 1 || a == -1) {
+        ok = parse(node[1], c * a.sgn(), negated);
       } else {
         ok = false;
       }
@@ -152,7 +152,7 @@ bool IDLAssertion::parse(TNode node, int c, bool negated) {
 
   case kind::PLUS: {
     for(unsigned i = 0; i < node.getNumChildren(); ++i) {
-      bool ok = parse(node[i], c, negated);
+      ok = parse(node[i], c, negated);
       if(!ok) {
         break;
       }
@@ -162,7 +162,7 @@ bool IDLAssertion::parse(TNode node, int c, bool negated) {
 
   case kind::MINUS: {
     ok = parse(node[0], c, negated);
-    if(ok) {
+    if (ok) {
       ok = parse(node[1], -c, negated);
     }
     break;
@@ -174,14 +174,14 @@ bool IDLAssertion::parse(TNode node, int c, bool negated) {
   }
 
   default: {
-    if(c > 0) {
-      if(d_x.isNull()) {
+    if (c > 0) {
+      if (d_x.isNull()) {
         d_x = node;
       } else {
         ok = false;
       }
     } else {
-      if(d_y.isNull()) {
+      if (d_y.isNull()) {
         d_y = node;
       } else {
         ok = false;