From 56b9799b4e4f7e13a6fbacf056a68fa04d52f018 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 10 Nov 2025 12:33:33 +0000 Subject: [PATCH] Incremental SMT2 back-end: support _Bool casts Added an extra case in `extension_for_type` to handle conversion between C boolean types and C integers by using zero extension. Fixes: #8069 --- regression/cbmc/Bool/bool2.desc | 2 +- regression/cbmc/Bool/bool3.desc | 2 +- regression/cbmc/c99_Bool/test.desc | 2 +- src/solvers/smt2_incremental/convert_expr_to_smt.cpp | 2 ++ 4 files changed, 5 insertions(+), 3 deletions(-) diff --git a/regression/cbmc/Bool/bool2.desc b/regression/cbmc/Bool/bool2.desc index e298f35dce1..e1e55611867 100644 --- a/regression/cbmc/Bool/bool2.desc +++ b/regression/cbmc/Bool/bool2.desc @@ -1,4 +1,4 @@ -CORE no-new-smt +CORE bool2.c ^EXIT=0$ diff --git a/regression/cbmc/Bool/bool3.desc b/regression/cbmc/Bool/bool3.desc index 2cd8843c88c..ab33f1f0312 100644 --- a/regression/cbmc/Bool/bool3.desc +++ b/regression/cbmc/Bool/bool3.desc @@ -1,4 +1,4 @@ -CORE no-new-smt +CORE bool3.c --json-ui ^EXIT=10$ diff --git a/regression/cbmc/c99_Bool/test.desc b/regression/cbmc/c99_Bool/test.desc index 9afc07ce007..a454c448ed0 100644 --- a/regression/cbmc/c99_Bool/test.desc +++ b/regression/cbmc/c99_Bool/test.desc @@ -1,4 +1,4 @@ -CORE no-new-smt +CORE main.c --function foo ^EXIT=0$ diff --git a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp index d5910628470..97dfa97bb43 100644 --- a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -167,6 +167,8 @@ extension_for_type(const typet &type) return smt_bit_vector_theoryt::zero_extend; if(can_cast_type(type)) return smt_bit_vector_theoryt::zero_extend; + if(can_cast_type(type)) + return smt_bit_vector_theoryt::zero_extend; UNREACHABLE; }