Remove spurious assertion in nonlinear extension (#1972)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 24 May 2018 01:41:11 +0000 (20:41 -0500)
committerGitHub <noreply@github.com>
Thu, 24 May 2018 01:41:11 +0000 (20:41 -0500)
src/theory/arith/nonlinear_extension.cpp

index 2ad79ac578ebd9c34ad6e1e967090aecc21c867b..c9a4c5075f84b61d6433521cb668e27b86757b57 100644 (file)
@@ -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++)
   {