diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-13 11:52:13 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-13 09:52:13 -0700 |
| commit | 3e96419d27621be3c0c0d4f3af4b14afb0ce24a8 (patch) | |
| tree | e0367d2bdf1578c1f0e9d2551b13be0c76419597 /src/theory/quantifiers/sygus_sampler.cpp | |
| parent | 3e7c4419ac051902b83343e25b123eee3b715059 (diff) | |
Fix case of non-constant value for sygus sampling (#4051)
Fixes #4050.
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; |