diff options
| author | Clark Barrett <barrett@cs.nyu.edu> | 2015-06-14 08:50:12 -0700 |
|---|---|---|
| committer | Clark Barrett <barrett@cs.nyu.edu> | 2015-06-14 08:50:12 -0700 |
| commit | 9bd95f1ffdb7108bc4990f48b9cf7d8a7bfb96b0 (patch) | |
| tree | 9c97aed371eead5914acddbcc1c008490f0b10a2 /src | |
| parent | cba911ca62d5a4eaa386f3e1f20fb37f776e0f58 (diff) | |
Fix for UMINUS translation in intToBV pass
Diffstat (limited to 'src')
| -rw-r--r-- | src/smt/smt_engine.cpp | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 99467b03a..e9d128ae0 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -2059,6 +2059,7 @@ Node SmtEnginePrivate::intToBV(TNode n, NodeMap& cache) { case kind::UMINUS: Assert(children.size() == 1); newKind = kind::BITVECTOR_NEG; + max = max + 1; break; case kind::LT: newKind = kind::BITVECTOR_SLT; |