projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: b1140ff) | patch
api: Require size argument for mkBitVector. (#6998)
authorAina Niemetz <aina.niemetz@gmail.com>
Mon, 23 Aug 2021 16:50:06 +0000 (09:50 -0700)
committerGitHub <noreply@github.com>
Mon, 23 Aug 2021 16:50:06 +0000 (16:50 +0000)
commit99af3afc7e1cd80b62e151fb7c35cee7cf08d785
tree86fa30517186044643951e66a24023a6478414a3tree
parentb1140ffab5d45f282417c4e9378ffbf5959f4673commit | diff
api: Require size argument for mkBitVector. (#6998)

This removes support for creating bit-vectors from a string without a
size argument. We further also now require that the base argument is
always given (it has no default value).
examples/api/python/floating_point.py diff | blob | history
src/api/cpp/cvc5.cpp diff | blob | history
src/api/cpp/cvc5.h diff | blob | history
src/api/python/cvc5.pxi diff | blob | history
src/parser/cvc/Cvc.g diff | blob | history
src/parser/smt2/Smt2.g diff | blob | history
test/python/unit/api/test_solver.py diff | blob | history
test/python/unit/api/test_term.py diff | blob | history
test/unit/api/solver_black.cpp diff | blob | history
test/unit/api/term_black.cpp diff | blob | history