projects
/
cvc5.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
| inline |
side by side
(parent:
55fd415
)
Remove spurious assertion in nonlinear extension (#1972)
author
Andrew Reynolds
<andrew.j.reynolds@gmail.com>
Thu, 24 May 2018 01:41:11 +0000
(20:41 -0500)
committer
GitHub
<noreply@github.com>
Thu, 24 May 2018 01:41:11 +0000
(20:41 -0500)
src/theory/arith/nonlinear_extension.cpp
patch
|
blob
|
history
diff --git
a/src/theory/arith/nonlinear_extension.cpp
b/src/theory/arith/nonlinear_extension.cpp
index 2ad79ac578ebd9c34ad6e1e967090aecc21c867b..c9a4c5075f84b61d6433521cb668e27b86757b57 100644
(file)
--- 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++)
{