diff options
Diffstat (limited to 'src/theory/arith/theory_arith.cpp')
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index ca2d74cf7..e159c0e42 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -1925,17 +1925,17 @@ DeltaRational TheoryArith::getDeltaValue(TNode n) { } } -void TheoryArith::collectModelInfo( TheoryModel* m ){ +void TheoryArith::collectModelInfo( TheoryModel* m, bool fullModel ){ Assert(d_qflraStatus == Result::SAT); - Debug("arith::collectModelInfo") << "collectModelInfo() begin " << endl; + Debug("arith::collectModelInfo") << "collectModelInfo() begin " << endl; // Delta lasts at least the duration of the function call const Rational& delta = d_partialModel.getDelta(); // TODO: // This is not very good for user push/pop.... - // Revisit when implementing push/pop + // Revisit when implementing push/pop for(ArithVar v = 0; v < d_variables.size(); ++v){ if(!isSlackVariable(v)){ Node term = d_arithvarNodeMap.asNode(v); |