Merge pull request #8044 from thomasspriggs/tas/fix_count_trailing_zeros_invariant

thomasspriggs · web-flow · commit bf6d75981324 · 2023-11-17T15:10:48.000Z
Fix the invariant message for unimplemented SMT count trailing zeros conversion.
diff --git 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());
 }
 

Original file line number	Diff line number	Diff line change
`@@ -1462,7 +1462,7 @@ static smt_termt convert_expr_to_smt(`
`1462`	`1462`	`const sub_expression_mapt &converted)`
`1463`	`1463`	`{`
`1464`	`1464`	`UNIMPLEMENTED_FEATURE(`
`1465`		`- "Generation of SMT formula for byte swap expression: " +`
	`1465`	`+ "Generation of SMT formula for count trailing zeros expression: " +`
`1466`	`1466`	`count_trailing_zeros.pretty());`
`1467`	`1467`	`}`
`1468`	`1468`