projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a6b48af) | patch
int-blaster: not allowing higher order functions (#8674)
authoryoni206 <yoni206@users.noreply.github.com>
Thu, 28 Apr 2022 17:08:43 +0000 (20:08 +0300)
committerGitHub <noreply@github.com>
Thu, 28 Apr 2022 17:08:43 +0000 (17:08 +0000)
commitb551a2b5d950f495d9309cb754c9c89abda95ffa
treec13602555c5f3cc8bc47ab92b8399849223bf7fatree
parenta6b48affa1382dc9b307e2c82dc5a16eac549d08commit | diff
int-blaster: not allowing higher order functions (#8674)

Currently we throw an OptionException if higher order logic is enabled, but we only check this once we reach an APPLY_FUN node.
This PR does the check regardless of APPLY_FUN, thus capturing, e.g. BAG_MAP.
Fixes cvc5/cvc5-projects#415.
The PR also includes a simplified version of the test from that issue.
src/theory/bv/int_blaster.cpp diff | blob | history
test/regress/cli/CMakeLists.txt diff | blob | history
test/regress/cli/regress0/bv/bv_to_int_415.smt2 [new file with mode: 0644] blob