From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 27 Sep 2018 19:40:06 +0000 (-0500)
Subject: Remove assertion. (#2549)
X-Git-Tag: cvc5-1.0.0~4489
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4a9e21371a5012285114126cab1dbce18fdcec6c;p=cvc5.git

Remove assertion. (#2549)
---

diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index dea67b7c3..99f1131fe 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -639,7 +639,6 @@ bool SynthConjecture::getEnumeratedValues(std::vector<Node>& n,
 
 Node SynthConjecture::getEnumeratedValue(Node e)
 {
-  Assert(d_tds->isEnumerator(e));
   if (e.getAttribute(SygusSymBreakExcAttribute()))
   {
     // if the current model value of e was excluded by symmetry breaking, then