projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 442ab0c) | patch
Handle cases in --sygus-rr where evaluation is not constant (#4100)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 16 Mar 2020 04:51:51 +0000 (23:51 -0500)
committerGitHub <noreply@github.com>
Mon, 16 Mar 2020 04:51:51 +0000 (21:51 -0700)
commit227cd8c26c508b7b444fbed6f2868f90c8281eed
treef48f18c8bda3c4ad448c711a7316f813c3819cb4tree
parent442ab0cdd8578631974318c17dd8ace59d145839commit | diff
Handle cases in --sygus-rr where evaluation is not constant (#4100)

Throws warning instead of error if two terms with the same rewritten form evaluate differently, but the evaluation is non-constant.

Fixes #4096 and fixes #4089.
src/theory/quantifiers/sygus_sampler.cpp diff | blob | history