From 79795539f7674981319f2d1f44582fe6a154bc50 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Fri, 17 Nov 2023 13:41:31 +0000 Subject: [PATCH] Fix INVARIANT message for unimplemented count trailing zeros Because this previously yielded a byte swap message which does not match the kind of expresion which triggers it. --- src/solvers/smt2_incremental/convert_expr_to_smt.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp index d9ddfa62d20..2d5b38879ba 100644 --- a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -1462,7 +1462,7 @@ static smt_termt convert_expr_to_smt( const sub_expression_mapt &converted) { UNIMPLEMENTED_FEATURE( - "Generation of SMT formula for byte swap expression: " + + "Generation of SMT formula for count trailing zeros expression: " + count_trailing_zeros.pretty()); }