summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/sygus/sygus_grammar_red.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/sygus/sygus_grammar_red.cpp')
-rw-r--r--src/theory/quantifiers/sygus/sygus_grammar_red.cpp1
1 files changed, 0 insertions, 1 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp
index 6ad590f28..2b2c87f38 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp
@@ -43,7 +43,6 @@ void SygusRedundantCons::initialize(QuantifiersEngine* qe, TypeNode tn)
std::map<int, Node> pre;
Node g = tds->mkGeneric(dt, i, pre);
Trace("sygus-red-debug") << " ...pre-rewrite : " << g << std::endl;
- Assert(g.getNumChildren() == dt[i].getNumArgs());
d_gen_terms[i] = g;
for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
{
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback