diff options
| author | yoni206 <yoni206@users.noreply.github.com> | 2021-01-08 07:08:05 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-01-08 09:08:05 -0600 |
| commit | 819eedc38031d3befb9c3e855bbbfa0afa3bb3cc (patch) | |
| tree | b46343ac3cfb562dcc964d5c596d59b4199a559b /src/theory/strings/base_solver.h | |
| parent | 497a685f14ff12eb05e4aa6ad7b05682609bf7a9 (diff) | |
bv-to-int: avoid binarizing nodes twice (#5749)
In bv-to-int, we first binarize the applications of associative-commutative operators (like bvadd etc.).
With this PR, we first check whether we already binarized a node, and only if we didn't, we perform binarization.
Diffstat (limited to 'src/theory/strings/base_solver.h')
0 files changed, 0 insertions, 0 deletions