1 files changed, 6 insertions, 2 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index b3eaec1fd..b2d43ac51 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2863,8 +2863,12 @@ Node SmtEnginePrivate::intToBV(TNode n, NodeMap& cache) {
               AlwaysAssert(constant.isIntegral());
               AlwaysAssert(constant >= 0);
               BitVector bv(size, constant.getNumerator());
-              if (bv.toSignedInt() != constant.getNumerator()) {
-                throw TypeCheckingException(current.toExpr(), string("Not enough bits for constant in intToBV: ") + current.toString());
+              if (bv.toSignedInteger() != constant.getNumerator())
+              {
+                throw TypeCheckingException(
+                    current.toExpr(),
+                    string("Not enough bits for constant in intToBV: ")
+                        + current.toString());
               }
               result = nm->mkConst(bv);
               break;