From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 24 May 2018 01:41:11 +0000 (-0500)
Subject: Remove spurious assertion in nonlinear extension (#1972)
X-Git-Tag: cvc5-1.0.0~5016
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=78b986c8c45159c1a6669602ec724dbfa2a5047b;p=cvc5.git

Remove spurious assertion in nonlinear extension (#1972)
---

diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp
index 2ad79ac57..c9a4c5075 100644
--- a/src/theory/arith/nonlinear_extension.cpp
+++ b/src/theory/arith/nonlinear_extension.cpp
@@ -1038,7 +1038,6 @@ bool NonlinearExtension::checkModel(const std::vector<Node>& assertions,
 void NonlinearExtension::addCheckModelSubstitution(TNode v, TNode s)
 {
   // should not substitute the same variable twice
-  Assert(v.isVar());
   Assert(!hasCheckModelAssignment(v));
   for (unsigned i = 0, size = d_check_model_subs.size(); i < size; i++)
   {