Adding a check in Polynomial::parsePolynomial to better enforce the arithmetic normal form when assertions are enabled.

1 files changed, 16 insertions, 2 deletions

diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h
index a182bc3b0..a1a33fed0 100644
--- a/src/theory/arith/normal_form.h
+++ b/src/theory/arith/normal_form.h
@@ -570,10 +570,24 @@ public:
       return true;
     }else if(n.getKind() == kind::PLUS){
       Assert(n.getNumChildren() >= 2);
-      for(Node::iterator curr = n.begin(), end = n.end(); curr != end;++curr){
-        if(!Monomial::isMember(*curr)){
+      Node::iterator currIter = n.begin(), end = n.end();
+      Node prev = *currIter;
+      if(!Monomial::isMember(prev)){
+        return false;
+      }
+
+      Monomial mprev = Monomial::parseMonomial(prev);
+      ++currIter;
+      for(; currIter != end; ++currIter){
+        Node curr = *currIter;
+        if(!Monomial::isMember(curr)){
+          return false;
+        }
+        Monomial mcurr = Monomial::parseMonomial(curr);
+        if(!(mprev < mcurr)){
           return false;
         }
+        mprev = mcurr;
       }
       return true;
     } else {