projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: d862942) | patch
SyGuS must use total bitvector division (#4119)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 19 Mar 2020 08:37:26 +0000 (03:37 -0500)
committerGitHub <noreply@github.com>
Thu, 19 Mar 2020 08:37:26 +0000 (01:37 -0700)
commit94844fbf4fbe4fa08d8fa4cbe093ba532f5bd613
treefb02a35e8ab26468f02e373ccab13bd710dfd6d5tree
parentd862942f821ea14973207ef538be3326fb11c17ccommit | diff
SyGuS must use total bitvector division (#4119)

Our SyGuS utilities are not designed to deal with partial bitvector division. If a user forced an older version of SMT-LIB semantics while using SyGuS, this led to a number of issues.

For now, we disable this option when it is combined with SyGuS, regardless of whether the user turns it on.

A more permanent solution will be to remove the old SMT-LIB semantics option bv-div-zero-const entirely.

Fixes #4097 and fixes #4088 and fixes #4104.
src/smt/smt_engine.cpp diff | blob | history