From 3e96419d27621be3c0c0d4f3af4b14afb0ce24a8 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 13 Mar 2020 11:52:13 -0500 Subject: [PATCH] Fix case of non-constant value for sygus sampling (#4051) Fixes #4050. --- src/theory/quantifiers/sygus_sampler.cpp | 8 ++++++-- 1 file 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; -- 2.30.2