franck44 / scalaSMT / issues / #14 - Support extract and concat for bitvectors — Bitbucket

Issue #14 resolved

Tony Sloane created an issue 2018-03-07

Currently extract is there in the grammar to some extent and terms can be created but this appears not to be fully tested with the solvers.

concat of bit vectors is not present at all.

Comments (3)

Franck Cassez repo owner
add tests for parsing extract and other BV functions. Some BV operations BVxxxTerm are production rules for Term and this may need fixing.
- 2018-03-07T23:52:36+00:00
Franck Cassez repo owner
tests for parsing BV operators added.
- 2018-03-08T06:33:43+00:00
Franck Cassez repo owner
- changed status to resolved
Add tests for concat and extract.

fixes ~~#14~~

→ <<cset a673ea8e8303>>
- 2018-03-08T07:48:10+00:00
Log in to comment

Assignee: Franck Cassez

Type: enhancement

Priority: major

Status: resolved

Votes: 0

Watchers: 2

Jira: the preferred issue tracker for Bitbucket. Join the team!