projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5de97c3) | patch
BV: Add missing type check for INT_TO_BITVECTOR. (#4613)
authorAina Niemetz <aina.niemetz@gmail.com>
Mon, 15 Jun 2020 18:48:02 +0000 (11:48 -0700)
committerGitHub <noreply@github.com>
Mon, 15 Jun 2020 18:48:02 +0000 (11:48 -0700)
commitaf37e2c948c140dbee2421a3cb046e068cc5b0f8
treea40c4ec35f088ae4877df774dccaa068bd8065a2tree
parent5de97c3efe8794bf7e39774686dca81a1982a8edcommit | diff
BV: Add missing type check for INT_TO_BITVECTOR. (#4613)

Fixes #4130.
This further makes an attempt at more consistent error printing.
src/main/main.cpp diff | blob | history
src/theory/bv/theory_bv_type_rules.h diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/bv/issue-4130.smt2 [new file with mode: 0644] blob
test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy diff | blob | history