diff options
| author | yoni206 <yoni206@users.noreply.github.com> | 2020-08-28 14:42:51 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-08-28 16:42:51 -0500 |
| commit | 48dfcfd271ff9fa04766e29fb82ba83290da1ad8 (patch) | |
| tree | c187227cf376e9202c509a0fc05da500a427ac06 /test/regress/regress0/bv | |
| parent | f51d3e353fe8e50e5e73c37c17229e603a56ecdd (diff) | |
Incremental support for bv_to_int (#4967)
This PR adds support for incremental solving in bv_to_int.
This amounts to:
using context dependent data structures
adding a test
In addition, we check for parametrized operations in a more robust way (using kind::metakind::PARAMETERIZED) and rename some tests for convenience.
Diffstat (limited to 'test/regress/regress0/bv')
| -rw-r--r-- | test/regress/regress0/bv/bv_to_int_bvuf_to_intuf.smt2 (renamed from test/regress/regress0/bv/bvuf_to_intuf.smt2) | 0 | ||||
| -rw-r--r-- | test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_smtlib.smt2 (renamed from test/regress/regress0/bv/bvuf_to_intuf_smtlib.smt2) | 0 | ||||
| -rw-r--r-- | test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2 (renamed from test/regress/regress0/bv/bvuf_to_intuf_sorts.smt2) | 0 |
3 files changed, 0 insertions, 0 deletions
diff --git a/test/regress/regress0/bv/bvuf_to_intuf.smt2 b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf.smt2 index c621aa112..c621aa112 100644 --- a/test/regress/regress0/bv/bvuf_to_intuf.smt2 +++ b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf.smt2 diff --git a/test/regress/regress0/bv/bvuf_to_intuf_smtlib.smt2 b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_smtlib.smt2 index 6196b2bb9..6196b2bb9 100644 --- a/test/regress/regress0/bv/bvuf_to_intuf_smtlib.smt2 +++ b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_smtlib.smt2 diff --git a/test/regress/regress0/bv/bvuf_to_intuf_sorts.smt2 b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2 index 8fbe96eab..8fbe96eab 100644 --- a/test/regress/regress0/bv/bvuf_to_intuf_sorts.smt2 +++ b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2 |