From: Tim King <taking@cs.nyu.edu>
Date: Sun, 14 Jun 2015 22:28:10 +0000 (+0200)
Subject: Fixing an assertion Constraint::assertionFringe(...) to allow hasTrichotomyProof().
X-Git-Tag: cvc5-1.0.0~6273
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=da4276464f90ffd091cc98ee1f74412018481eb3;p=cvc5.git

Fixing an assertion Constraint::assertionFringe(...) to allow hasTrichotomyProof().
---

diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index 822f0e578..f1cac9044 100644
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -1346,7 +1346,7 @@ void Constraint::assertionFringe(ConstraintCPVec& v){
           v[writePos] = vi;
           writePos++;
         }else{
-          Assert(vi->hasFarkasProof() || vi->hasIntHoleProof() );
+          Assert(vi->hasTrichotomyProof() || vi->hasFarkasProof() || vi->hasIntHoleProof() );
           AntecedentId p = vi->getEndAntecedent();
 
           ConstraintCP antecedent = antecedents[p];