From 5a85b3a4dd4aa04b3efab19b52c274bf6268cf00 Mon Sep 17 00:00:00 2001 From: Yoni Zohar Date: Fri, 6 Oct 2023 16:07:59 +0300 Subject: [PATCH] doc --- src/preprocessing/passes/int_to_bv.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/preprocessing/passes/int_to_bv.cpp b/src/preprocessing/passes/int_to_bv.cpp index f18a9170f21..9ca1cebdb37 100644 --- a/src/preprocessing/passes/int_to_bv.cpp +++ b/src/preprocessing/passes/int_to_bv.cpp @@ -206,7 +206,11 @@ Node IntToBV::intToBV(TNode n, NodeMap& cache) } } } - + + // abort if the kind did not change and + // the original type was integer. + // The only exception is an ITE, + // in which case we continue. if (tn.isInteger() && newKind != Kind::ITE && newKind == current.getKind()) {