diff options
| author | yoni206 <yoni206@users.noreply.github.com> | 2020-07-11 04:39:56 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-07-11 06:39:56 -0500 |
| commit | c481454a4b05a78ea99e835ec7427a719a2d5c77 (patch) | |
| tree | 9e1b3d680f2ffe418317c014fd4e733ff68cc0a5 /src/preprocessing/passes | |
| parent | 9aab4da2460b62273ac937ad96b7b6695b904e0d (diff) | |
Changing bv_to_int options (#4721)
This PR changes --solve-bv-as-int from a numerical option (specifying the granularity) to an enum (specifying the approach). Currently we support only two modes: OFF and SUM. Future PRs will add more modes.
The numerical value of the granularity is now captured by the new option --bvand-integer-granularity.
Tests are updated accordingly.
Diffstat (limited to 'src/preprocessing/passes')
| -rw-r--r-- | src/preprocessing/passes/bv_to_int.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp index 5b125b4b6..bb0bde2f9 100644 --- a/src/preprocessing/passes/bv_to_int.cpp +++ b/src/preprocessing/passes/bv_to_int.cpp @@ -269,7 +269,7 @@ Node BVToInt::bvToInt(Node n) n = makeBinary(n); vector<Node> toVisit; toVisit.push_back(n); - uint64_t granularity = options::solveBVAsInt(); + uint64_t granularity = options::BVAndIntegerGranularity(); while (!toVisit.empty()) { |