diff options
Diffstat (limited to 'src/theory/quantifiers/sygus_sampler.cpp')
-rw-r--r-- | src/theory/quantifiers/sygus_sampler.cpp | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp index 10af0d703..d2c2a2380 100644 --- a/src/theory/quantifiers/sygus_sampler.cpp +++ b/src/theory/quantifiers/sygus_sampler.cpp @@ -713,8 +713,12 @@ Node SygusSampler::getSygusRandomValue(TypeNode tn, Trace("sygus-sample-grammar") << "...returned " << ret << std::endl; ret = Rewriter::rewrite(ret); Trace("sygus-sample-grammar") << "...after rewrite " << ret << std::endl; - Assert(ret.isConst()); - return ret; + // A rare case where we generate a non-constant value from constant + // leaves is (/ n 0). + if(ret.isConst()) + { + return ret; + } } } Trace("sygus-sample-grammar") << "...resort to random value" << std::endl; |