From 9290b5c8200a5b398ff59dff0ecbc929bd7317df Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 26 Nov 2025 09:44:00 +0000
Subject: [PATCH 01/14] Enable Clang sanitizers in Linux/Clang CI pipeline

Adds a dedicated CI job that runs unit and regression tests on Ubuntu
24.04 after compiling with Clang's sanitizers. Enables address sanitizer
(buffer overflow, use-after-free, use-after-return, double-free), memory
leak sanitizer, and undefined-behavior sanitizer (integer overflow).

- [AddressSanitizer Documentation](https://clang.llvm.org/docs/AddressSanitizer.html)
- [LeakSanitizer Documentation](https://clang.llvm.org/docs/LeakSanitizer.html)
- [UndefinedBehaviorSanitizer Documentation](https://clang.llvm.org/docs/UndefinedBehaviorSanitizer.html)

Fixes: #832
---
 .github/workflows/clang-sanitizer.yaml | 92 ++++++++++++++++++++++++++
 1 file changed, 92 insertions(+)
 create mode 100644 .github/workflows/clang-sanitizer.yaml

diff --git a/.github/workflows/clang-sanitizer.yaml b/.github/workflows/clang-sanitizer.yaml
new file mode 100644
index 00000000000..4622e867c3a
--- /dev/null
+++ b/.github/workflows/clang-sanitizer.yaml
@@ -0,0 +1,92 @@
+name: Clang Sanitizer
+on:
+  push:
+    branches: [ develop ]
+  pull_request:
+    branches: [ develop ]
+env:
+  cvc5-version: "1.2.1"
+  linux-vcpus: 4
+
+jobs:
+  # This job takes approximately X to Y minutes
+  clang-asan-ubuntu-24_04-make:
+    runs-on: ubuntu-24.04
+    env:
+      CC: "ccache /usr/bin/clang"
+      CXX: "ccache /usr/bin/clang++"
+      # AddressSanitizer configuration for optimal CI performance
+      ASAN_OPTIONS: "abort_on_error=1:fast_unwind_on_malloc=0:detect_odr_violation=0:detect_leaks=1"
+      # - `abort_on_error=1`: Terminate immediately on error
+      # - `fast_unwind_on_malloc=0`: Use slower but more accurate stack unwinding
+      # - `detect_odr_violation=0`: Disable One Definition Rule violation detection to reduce noise
+      # - `detect_leaks=1`: Enable leak detection
+      UBSAN_OPTIONS: "print_stacktrace=1:halt_on_error=1"
+      # - `print_stacktrace=1`: Show stack traces for undefined behavior
+      # - `halt_on_error=1`: Terminate on undefined behavior
+    steps:
+      - uses: actions/checkout@v6
+        with:
+          submodules: recursive
+      - name: Fetch dependencies
+        env:
+          DEBIAN_FRONTEND: noninteractive
+        run: |
+          sudo apt-get update
+          sudo apt-get install --no-install-recommends -yq clang-19 clang++-19 gdb maven jq flex bison libxml2-utils ccache z3
+          make -C src minisat2-download
+      - name: Confirm z3 solver is available and log the version installed
+        run: z3 --version
+      - name: Download cvc-5 from the releases page and make sure it can be deployed
+        run: |
+          wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux-x86_64-static.zip
+          unzip -j -d /usr/local/bin cvc5-Linux-x86_64-static.zip cvc5-Linux-x86_64-static/bin/cvc5
+          rm cvc5-Linux-x86_64-static.zip
+          cvc5 --version
+      - name: Prepare ccache
+        uses: actions/cache@v4
+        with:
+          save-always: true
+          path: .ccache
+          key: ${{ runner.os }}-24.04-make-clang-asan-${{ github.ref }}-${{ github.sha }}-PR
+          restore-keys: |
+            ${{ runner.os }}-24.04-make-clang-asan-${{ github.ref }}
+            ${{ runner.os }}-24.04-make-clang-asan
+      - name: ccache environment
+        run: |
+          echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
+          echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
+      - name: Zero ccache stats and limit in size
+        run: ccache -z --max-size=500M
+      - name: Build with AddressSanitizer and LeakSanitizer
+        run: |
+          # Build with sanitizers enabled - using -O1 for reasonable performance
+          # -fsanitize=address: detects buffer overflows, use-after-free, etc.
+          # -fsanitize=leak: detects memory leaks
+          # -fsanitize=undefined: detects undefined behavior
+          # -fno-sanitize-recover=all: abort on first error for faster feedback
+          # -g: include debug symbols for better error reporting
+          export SANITIZER_FLAGS="-fsanitize=address -fsanitize=leak -fsanitize=undefined -fno-sanitize-recover=all -g -O1"
+          make -C src -j${{env.linux-vcpus}} \
+            CXXFLAGS="$SANITIZER_FLAGS" \
+            LINKFLAGS="$SANITIZER_FLAGS" \
+            MINISAT2=../../minisat-2.2.1
+          make -C unit -j${{env.linux-vcpus}} \
+            CXXFLAGS="$SANITIZER_FLAGS" \
+            LINKFLAGS="$SANITIZER_FLAGS"
+      - name: Print ccache stats
+        run: ccache -s
+      - name: Run unit tests
+        run: |
+          make -C unit test
+          make -C jbmc/unit test
+          echo "Running expected failure tests"
+          make TAGS="[!shouldfail]" -C unit test
+          make TAGS="[!shouldfail]" -C jbmc/unit test
+      - name: Run regression tests
+        run: |
+          export PATH=$PATH:`pwd`/src/solvers
+          make -C regression test-parallel JOBS=${{env.linux-vcpus}}
+          make -C regression/cbmc test-paths-lifo
+          make -C regression/cbmc test-cprover-smt2
+          make -C jbmc/regression test-parallel JOBS=${{env.linux-vcpus}}

From 44b2176afedf6d995d656f60f3da4120115f3758 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Sun, 30 Nov 2025 12:50:49 +0000
Subject: [PATCH 02/14] Do not use value-set supported simplification with
 multiple threads

Shared pointers may be updated in yet-to-be-executed threads.
---
 src/goto-symex/goto_symex.cpp              | 13 ++++++++++---
 src/goto-symex/goto_symex.h                |  2 +-
 src/goto-symex/symex_atomic_section.cpp    |  4 ++--
 src/goto-symex/symex_builtin_functions.cpp |  8 ++++----
 src/goto-symex/symex_clean_expr.cpp        |  4 ++--
 src/goto-symex/symex_dereference.cpp       |  8 ++++----
 src/goto-symex/symex_goto.cpp              |  2 +-
 src/goto-symex/symex_main.cpp              | 10 +++++-----
 src/goto-symex/symex_other.cpp             |  6 +++---
 9 files changed, 32 insertions(+), 25 deletions(-)

diff --git a/src/goto-symex/goto_symex.cpp b/src/goto-symex/goto_symex.cpp
index 24d9e4dc33b..0c0efb5106a 100644
--- a/src/goto-symex/goto_symex.cpp
+++ b/src/goto-symex/goto_symex.cpp
@@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/mathematical_expr.h>
 #include <util/mathematical_types.h>
 #include <util/pointer_offset_size.h>
+#include <util/simplify_expr.h>
 #include <util/simplify_utils.h>
 #include <util/std_code.h>
 #include <util/string_expr.h>
@@ -29,11 +30,17 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <climits>
 
-void goto_symext::do_simplify(exprt &expr, const value_sett &value_set)
+void goto_symext::do_simplify(exprt &expr, const statet &state)
 {
   if(symex_config.simplify_opt)
   {
-    simplify_expr_with_value_sett{value_set, language_mode, ns}.simplify(expr);
+    if(state.threads.size() == 1)
+    {
+      simplify_expr_with_value_sett{state.value_set, language_mode, ns}
+        .simplify(expr);
+    }
+    else
+      simplify(expr, ns);
   }
 }
 
@@ -63,7 +70,7 @@ void goto_symext::symex_assign(
   // "byte_extract <type> from an_lvalue offset this_rvalue") can affect whether
   // we use field-sensitive symbols or not, so L2-rename them up front:
   lhs = state.l2_rename_rvalues(lhs, ns);
-  do_simplify(lhs, state.value_set);
+  do_simplify(lhs, state);
   lhs = state.field_sensitivity.apply(ns, state, std::move(lhs), true);
 
   if(rhs.id() == ID_side_effect)
diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h
index 5980573f0cd..2c36ef7e14c 100644
--- a/src/goto-symex/goto_symex.h
+++ b/src/goto-symex/goto_symex.h
@@ -526,7 +526,7 @@ class goto_symext
   /// \param state: Symbolic execution state for current instruction
   void symex_catch(statet &state);
 
-  virtual void do_simplify(exprt &expr, const value_sett &value_set);
+  virtual void do_simplify(exprt &expr, const statet &state);
 
   /// Symbolically execute an ASSIGN instruction or simulate such an execution
   /// for a synthetic assignment
diff --git a/src/goto-symex/symex_atomic_section.cpp b/src/goto-symex/symex_atomic_section.cpp
index 231c40303e7..45ee547abb6 100644
--- a/src/goto-symex/symex_atomic_section.cpp
+++ b/src/goto-symex/symex_atomic_section.cpp
@@ -58,7 +58,7 @@ void goto_symext::symex_atomic_end(statet &state)
         ++it)
       read_guard|=*it;
     exprt read_guard_expr=read_guard.as_expr();
-    do_simplify(read_guard_expr, state.value_set);
+    do_simplify(read_guard_expr, state);
 
     target.shared_read(
       read_guard_expr,
@@ -80,7 +80,7 @@ void goto_symext::symex_atomic_end(statet &state)
         ++it)
       write_guard|=*it;
     exprt write_guard_expr=write_guard.as_expr();
-    do_simplify(write_guard_expr, state.value_set);
+    do_simplify(write_guard_expr, state);
 
     target.shared_write(
       write_guard_expr,
diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp
index 0ffc7b606f6..c31bc0eab4d 100644
--- a/src/goto-symex/symex_builtin_functions.cpp
+++ b/src/goto-symex/symex_builtin_functions.cpp
@@ -293,7 +293,7 @@ void goto_symext::symex_va_start(
 
   array = clean_expr(std::move(array), state, false);
   array = state.rename(std::move(array), ns).get();
-  do_simplify(array, state.value_set);
+  do_simplify(array, state);
   symex_assign(state, va_array.symbol_expr(), std::move(array));
 
   exprt rhs = address_of_exprt{index_exprt{
@@ -388,7 +388,7 @@ void goto_symext::symex_printf(
   exprt tmp_rhs = rhs;
   clean_expr(tmp_rhs, state, false);
   tmp_rhs = state.rename(std::move(tmp_rhs), ns).get();
-  do_simplify(tmp_rhs, state.value_set);
+  do_simplify(tmp_rhs, state);
 
   const exprt::operandst &operands=tmp_rhs.operands();
   std::list<exprt> args;
@@ -426,7 +426,7 @@ void goto_symext::symex_printf(
         parameter = to_address_of_expr(parameter).object();
       clean_expr(parameter, state, false);
       parameter = state.rename(std::move(parameter), ns).get();
-      do_simplify(parameter, state.value_set);
+      do_simplify(parameter, state);
 
       args.push_back(std::move(parameter));
     }
@@ -454,7 +454,7 @@ void goto_symext::symex_input(
   for(std::size_t i=1; i<code.operands().size(); i++)
   {
     exprt l2_arg = state.rename(code.operands()[i], ns).get();
-    do_simplify(l2_arg, state.value_set);
+    do_simplify(l2_arg, state);
     args.emplace_back(std::move(l2_arg));
   }
 
diff --git a/src/goto-symex/symex_clean_expr.cpp b/src/goto-symex/symex_clean_expr.cpp
index f065dbda360..a650d97b707 100644
--- a/src/goto-symex/symex_clean_expr.cpp
+++ b/src/goto-symex/symex_clean_expr.cpp
@@ -135,7 +135,7 @@ void goto_symext::process_array_expr(statet &state, exprt &expr)
   lift_lets(state, expr);
 
   ::process_array_expr(expr, ns);
-  do_simplify(expr, state.value_set);
+  do_simplify(expr, state);
 }
 
 /// Rewrite index/member expressions in byte_extract to offset
@@ -178,7 +178,7 @@ void goto_symext::lift_let(statet &state, const let_exprt &let_expr)
 {
   exprt let_value = clean_expr(let_expr.value(), state, false);
   let_value = state.rename(std::move(let_value), ns).get();
-  do_simplify(let_value, state.value_set);
+  do_simplify(let_value, state);
 
   exprt::operandst value_assignment_guard;
   symex_assignt{
diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp
index 6948502b67e..69ff860f555 100644
--- a/src/goto-symex/symex_dereference.cpp
+++ b/src/goto-symex/symex_dereference.cpp
@@ -101,7 +101,7 @@ exprt goto_symext::address_arithmetic(
     // recursive call
     result = address_arithmetic(be, state, keep_array);
 
-    do_simplify(result, state.value_set);
+    do_simplify(result, state);
   }
   else if(expr.id()==ID_dereference)
   {
@@ -158,7 +158,7 @@ exprt goto_symext::address_arithmetic(
 
       result = address_arithmetic(be, state, keep_array);
 
-      do_simplify(result, state.value_set);
+      do_simplify(result, state);
     }
     else
       result=address_of_exprt(result);
@@ -308,7 +308,7 @@ void goto_symext::dereference_rec(
 
     tmp1 = state.rename<L1_WITH_CONSTANT_PROPAGATION>(tmp1, ns).get();
 
-    do_simplify(tmp1, state.value_set);
+    do_simplify(tmp1, state);
 
     if(symex_config.run_validation_checks)
     {
@@ -515,7 +515,7 @@ void goto_symext::dereference(exprt &expr, statet &state, bool write)
   // when all we need is
   // s1 := s1 with (member := X) [and guard b]
   // s2 := s2 with (member := X) [and guard !b]
-  do_simplify(expr, state.value_set);
+  do_simplify(expr, state);
 
   if(symex_config.run_validation_checks)
   {
diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp
index 3bde290706b..ee725205ff3 100644
--- a/src/goto-symex/symex_goto.cpp
+++ b/src/goto-symex/symex_goto.cpp
@@ -118,7 +118,7 @@ void goto_symext::symex_goto(statet &state)
       // generate assume(false) or a suitable negation if this
       // instruction is a conditional goto
       exprt negated_guard = boolean_negate(new_guard);
-      do_simplify(negated_guard, state.value_set);
+      do_simplify(negated_guard, state);
       log.statistics() << "replacing self-loop at "
                        << state.source.pc->source_location() << " by assume("
                        << from_expr(ns, state.source.function_id, negated_guard)
diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp
index 4fe53bc7c61..f287a070c89 100644
--- a/src/goto-symex/symex_main.cpp
+++ b/src/goto-symex/symex_main.cpp
@@ -157,7 +157,7 @@ void goto_symext::symex_assert(
   // First, push negations in and perhaps convert existential quantifiers into
   // universals:
   if(has_subexpr(condition, ID_exists) || has_subexpr(condition, ID_forall))
-    do_simplify(condition, state.value_set);
+    do_simplify(condition, state);
 
   // Second, L2-rename universal quantifiers:
   if(has_subexpr(condition, ID_forall))
@@ -167,7 +167,7 @@ void goto_symext::symex_assert(
   exprt l2_condition = state.rename(std::move(condition), ns).get();
 
   // now try simplifier on it
-  do_simplify(l2_condition, state.value_set);
+  do_simplify(l2_condition, state);
 
   std::string msg = id2string(instruction.source_location().get_comment());
   if(msg.empty())
@@ -200,7 +200,7 @@ void goto_symext::symex_assume(statet &state, const exprt &cond)
 {
   exprt simplified_cond = clean_expr(cond, state, false);
   simplified_cond = state.rename(std::move(simplified_cond), ns).get();
-  do_simplify(simplified_cond, state.value_set);
+  do_simplify(simplified_cond, state);
 
   // It would be better to call try_filter_value_sets after apply_condition,
   // but it is not currently possible. See the comment at the beginning of
@@ -848,13 +848,13 @@ void goto_symext::try_filter_value_sets(
     // without another round of constant propagation.
     // It would be sufficient to replace this call to do_simplify() with
     // something that just replaces `*&x` with `x` whenever it finds it.
-    do_simplify(modified_condition, state.value_set);
+    do_simplify(modified_condition, state);
 
     state.record_events.push(false);
     modified_condition = state.rename(std::move(modified_condition), ns).get();
     state.record_events.pop();
 
-    do_simplify(modified_condition, state.value_set);
+    do_simplify(modified_condition, state);
 
     if(jump_taken_value_set && modified_condition == false)
     {
diff --git a/src/goto-symex/symex_other.cpp b/src/goto-symex/symex_other.cpp
index c5e046356bf..ee55abf9273 100644
--- a/src/goto-symex/symex_other.cpp
+++ b/src/goto-symex/symex_other.cpp
@@ -151,14 +151,14 @@ void goto_symext::symex_other(
       {
         src_array = make_byte_extract(
           src_array, from_integer(0, c_index_type()), dest_array.type());
-        do_simplify(src_array, state.value_set);
+        do_simplify(src_array, state);
       }
       else
       {
         // ID_array_replace
         dest_array = make_byte_extract(
           dest_array, from_integer(0, c_index_type()), src_array.type());
-        do_simplify(dest_array, state.value_set);
+        do_simplify(dest_array, state);
       }
     }
 
@@ -197,7 +197,7 @@ void goto_symext::symex_other(
     {
       auto array_size = size_of_expr(array_expr.type(), ns);
       CHECK_RETURN(array_size.has_value());
-      do_simplify(array_size.value(), state.value_set);
+      do_simplify(array_size.value(), state);
       array_expr = make_byte_extract(
         array_expr,
         from_integer(0, c_index_type()),

From 3f24c0becfe5b894c5315593ce61d0d74865b5ed Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Mon, 1 Dec 2025 18:15:53 +0000
Subject: [PATCH 03/14] Fix reference to temporary that has gone out of scope

Although the temporary is bound by a const reference, that reference is
then just passed on to subobject initialisers. Per
https://en.cppreference.com/w/cpp/language/reference_initialization.html#Lifetime_of_a_temporary,
"passing on" does not extend the lifetime of a temporary.

Try working around asan
---
 unit/goto-symex/goto_symex_state.cpp | 3 ++-
 unit/goto-symex/symex_assign.cpp     | 5 +++--
 2 files changed, 5 insertions(+), 3 deletions(-)

diff --git a/unit/goto-symex/goto_symex_state.cpp b/unit/goto-symex/goto_symex_state.cpp
index 9042248686e..35431145d48 100644
--- a/unit/goto-symex/goto_symex_state.cpp
+++ b/unit/goto-symex/goto_symex_state.cpp
@@ -38,11 +38,12 @@ SCENARIO(
   auto fresh_name = [&fresh_name_count](const irep_idt &) {
     return fresh_name_count++;
   };
+  const irep_idt empty_language_mode;
   goto_symex_statet state{
     source,
     DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE,
     true,
-    irep_idt{},
+    empty_language_mode,
     manager,
     fresh_name};
 
diff --git a/unit/goto-symex/symex_assign.cpp b/unit/goto-symex/symex_assign.cpp
index 3464c3ba7c2..c7785e0e693 100644
--- a/unit/goto-symex/symex_assign.cpp
+++ b/unit/goto-symex/symex_assign.cpp
@@ -48,11 +48,12 @@ SCENARIO(
   auto fresh_name = [&fresh_name_count](const irep_idt &) {
     return fresh_name_count++;
   };
+  const irep_idt empty_language_mode;
   goto_symex_statet state{
     source,
     DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE,
     true,
-    irep_idt{},
+    empty_language_mode,
     manager,
     fresh_name};
 
@@ -234,7 +235,7 @@ SCENARIO(
         symex_targett::assignment_typet::STATE,
         ns,
         symex_config,
-        irep_idt{},
+        empty_language_mode,
         target_equation}
         .assign_symbol(struct1_ssa, skeleton, rhs, guard);
       THEN("Two equations are added to the target")

From 65715aba47ab7ac4d5da6112232ceed97129d172 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Mon, 1 Dec 2025 19:04:03 +0000
Subject: [PATCH 04/14] Initialise all POD members of goto_symex_statet

The constructor did not take care of them and our unit tests exposed
that, at least within unit tests, we were accessing uninitialised
members.
---
 src/goto-symex/goto_symex_state.h | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h
index 96020d5970e..50a507cf1ac 100644
--- a/src/goto-symex/goto_symex_state.h
+++ b/src/goto-symex/goto_symex_state.h
@@ -68,7 +68,7 @@ class goto_symex_statet final : public goto_statet
 
   // Manager is required to be able to resize the thread vector
   guard_managert &guard_manager;
-  symex_target_equationt *symex_target;
+  symex_target_equationt *symex_target = nullptr;
 
   symex_level1t level1;
 
@@ -217,14 +217,14 @@ class goto_symex_statet final : public goto_statet
   goto_programt::const_targett saved_target;
 
   /// \brief This state is saved, with the PC pointing to the target of a GOTO
-  bool has_saved_jump_target;
+  bool has_saved_jump_target = false;
 
   /// \brief This state is saved, with the PC pointing to the next instruction
   /// of a GOTO
-  bool has_saved_next_instruction;
+  bool has_saved_next_instruction = false;
 
   /// \brief Should the additional validation checks be run?
-  bool run_validation_checks;
+  bool run_validation_checks = false;
 
   unsigned total_vccs = 0;
   unsigned remaining_vccs = 0;

From 6d3b8a16f9e514effdb42c26f7c0822fa89f1d81 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 2 Dec 2025 01:03:26 +0000
Subject: [PATCH 05/14] Remove language_mode from goto_symext

`goto_symex_statet` holds a reference to a language mode, which was
being initialised to `goto_symext::language_mode` in
`goto_symext::initialize_entry_point_state`. That `goto_symext` object,
however, may be the one created in
`single_path_symex_only_checkert::initialize_worklist`, whereupon the
`goto_symex_statet` will outlive it.

Fix this problem by getting rid of the `language_mode` member of
`goto_symext` and initialise `goto_symex_statet::language_mode` from a
mode in the symbol table, which outlives all goto-symex objects.
---
 src/goto-checker/symex_bmc.cpp             |  6 ------
 src/goto-symex/goto_symex.cpp              | 18 +++---------------
 src/goto-symex/goto_symex.h                |  4 ----
 src/goto-symex/goto_symex_state.h          |  5 ++++-
 src/goto-symex/symex_assign.cpp            |  4 ++--
 src/goto-symex/symex_assign.h              |  3 ---
 src/goto-symex/symex_builtin_functions.cpp | 17 +++++++++--------
 src/goto-symex/symex_clean_expr.cpp        |  3 +--
 src/goto-symex/symex_dereference.cpp       |  5 ++---
 src/goto-symex/symex_function_call.cpp     |  8 +-------
 src/goto-symex/symex_goto.cpp              |  3 ++-
 src/goto-symex/symex_main.cpp              |  4 ++--
 src/goto-symex/symex_start_thread.cpp      |  2 --
 unit/goto-symex/symex_assign.cpp           |  3 ---
 14 files changed, 26 insertions(+), 59 deletions(-)

diff --git a/src/goto-checker/symex_bmc.cpp b/src/goto-checker/symex_bmc.cpp
index cd99776aea2..2a5b3d9a0ea 100644
--- a/src/goto-checker/symex_bmc.cpp
+++ b/src/goto-checker/symex_bmc.cpp
@@ -16,8 +16,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <goto-programs/unwindset.h>
 
-#include <linking/static_lifetime_init.h>
-
 #include <limits>
 
 symex_bmct::symex_bmct(
@@ -40,10 +38,6 @@ symex_bmct::symex_bmct(
     unwindset(unwindset),
     symex_coverage(ns)
 {
-  const symbolt *init_symbol = outer_symbol_table.lookup(INITIALIZE_FUNCTION);
-  if(init_symbol)
-    language_mode = init_symbol->mode;
-
   messaget msg{mh};
   msg.status() << "Starting Bounded Model Checking" << messaget::eom;
 }
diff --git a/src/goto-symex/goto_symex.cpp b/src/goto-symex/goto_symex.cpp
index 0c0efb5106a..3bbbd2bfb41 100644
--- a/src/goto-symex/goto_symex.cpp
+++ b/src/goto-symex/goto_symex.cpp
@@ -36,7 +36,7 @@ void goto_symext::do_simplify(exprt &expr, const statet &state)
   {
     if(state.threads.size() == 1)
     {
-      simplify_expr_with_value_sett{state.value_set, language_mode, ns}
+      simplify_expr_with_value_sett{state.value_set, state.language_mode, ns}
         .simplify(expr);
     }
     else
@@ -113,13 +113,7 @@ void goto_symext::symex_assign(
       assignment_type = symex_targett::assignment_typet::HIDDEN;
 
     symex_assignt symex_assign{
-      shadow_memory,
-      state,
-      assignment_type,
-      ns,
-      symex_config,
-      language_mode,
-      target};
+      shadow_memory, state, assignment_type, ns, symex_config, target};
 
     // Try to constant propagate potential side effects of the assignment, when
     // simplification is turned on and there is one thread only. Constant
@@ -149,13 +143,7 @@ void goto_symext::symex_assign(
 
     exprt::operandst lhs_if_then_else_conditions;
     symex_assignt{
-      shadow_memory,
-      state,
-      assignment_type,
-      ns,
-      symex_config,
-      language_mode,
-      target}
+      shadow_memory, state, assignment_type, ns, symex_config, target}
       .assign_rec(lhs, expr_skeletont{}, rhs, lhs_if_then_else_conditions);
 
     if(need_atomic_section)
diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h
index 2c36ef7e14c..fc2d7525b1b 100644
--- a/src/goto-symex/goto_symex.h
+++ b/src/goto-symex/goto_symex.h
@@ -235,10 +235,6 @@ class goto_symext
   messaget::mstreamt &
   print_callstack_entry(const symex_targett::sourcet &target);
 
-  /// language_mode: ID_java, ID_C or another language identifier
-  /// if we know the source language in use, irep_idt() otherwise.
-  irep_idt language_mode;
-
   /// The symbol table associated with the goto-program being executed.
   /// This symbol table will not have objects that are dynamically created as
   /// part of symbolic execution added to it; those object are stored in the
diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h
index 50a507cf1ac..769b16ccec1 100644
--- a/src/goto-symex/goto_symex_state.h
+++ b/src/goto-symex/goto_symex_state.h
@@ -258,8 +258,11 @@ class goto_symex_statet final : public goto_statet
            lvalue.id() == ID_array;
   }
 
-private:
+  /// language_mode: ID_java, ID_C or another language identifier
+  /// if we know the source language in use, irep_idt() otherwise.
   const irep_idt &language_mode;
+
+private:
   std::function<std::size_t(const irep_idt &)> fresh_l2_name_provider;
 
   /// \brief Dangerous, do not use
diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp
index 15fd2358236..e685faf2670 100644
--- a/src/goto-symex/symex_assign.cpp
+++ b/src/goto-symex/symex_assign.cpp
@@ -207,8 +207,8 @@ void symex_assignt::assign_non_struct_symbol(
 
   if(symex_config.simplify_opt)
   {
-    simplify_expr_with_value_sett{state.value_set, language_mode, ns}.simplify(
-      assignment.rhs);
+    simplify_expr_with_value_sett{state.value_set, state.language_mode, ns}
+      .simplify(assignment.rhs);
   }
 
   const ssa_exprt l2_lhs = state
diff --git a/src/goto-symex/symex_assign.h b/src/goto-symex/symex_assign.h
index e6a282637d7..2d8fa1611a7 100644
--- a/src/goto-symex/symex_assign.h
+++ b/src/goto-symex/symex_assign.h
@@ -33,14 +33,12 @@ class symex_assignt
     symex_targett::assignment_typet assignment_type,
     const namespacet &ns,
     const symex_configt &symex_config,
-    const irep_idt &language_mode,
     symex_targett &target)
     : shadow_memory(shadow_memory),
       state(state),
       assignment_type(assignment_type),
       ns(ns),
       symex_config(symex_config),
-      language_mode(language_mode),
       target(target)
   {
   }
@@ -67,7 +65,6 @@ class symex_assignt
   symex_targett::assignment_typet assignment_type;
   const namespacet &ns;
   const symex_configt &symex_config;
-  const irep_idt &language_mode;
   symex_targett &target;
 
   void assign_from_struct(
diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp
index c31bc0eab4d..5e80be6d485 100644
--- a/src/goto-symex/symex_builtin_functions.cpp
+++ b/src/goto-symex/symex_builtin_functions.cpp
@@ -72,8 +72,8 @@ void goto_symext::symex_allocate(
   {
     // to allow constant propagation
     exprt tmp_size = state.rename(size, ns).get();
-    simplify_expr_with_value_sett{state.value_set, language_mode, ns}.simplify(
-      tmp_size);
+    simplify_expr_with_value_sett{state.value_set, state.language_mode, ns}
+      .simplify(tmp_size);
 
     // special treatment for sizeof(T)*x
     {
@@ -167,8 +167,8 @@ void goto_symext::symex_allocate(
 
   // to allow constant propagation
   exprt zero_init = state.rename(to_binary_expr(code).op1(), ns).get();
-  simplify_expr_with_value_sett{state.value_set, language_mode, ns}.simplify(
-    zero_init);
+  simplify_expr_with_value_sett{state.value_set, state.language_mode, ns}
+    .simplify(zero_init);
 
   INVARIANT(
     zero_init.is_constant(), "allocate expects constant as second argument");
@@ -433,7 +433,7 @@ void goto_symext::symex_printf(
   }
 
   const irep_idt format_string =
-    get_string_argument(operands[0], state.value_set, language_mode, ns);
+    get_string_argument(operands[0], state.value_set, state.language_mode, ns);
 
   if(!format_string.empty())
     target.output_fmt(
@@ -459,7 +459,7 @@ void goto_symext::symex_input(
   }
 
   const irep_idt input_id =
-    get_string_argument(id_arg, state.value_set, language_mode, ns);
+    get_string_argument(id_arg, state.value_set, state.language_mode, ns);
 
   target.input(state.guard.as_expr(), state.source, input_id, args);
 }
@@ -478,14 +478,15 @@ void goto_symext::symex_output(
     renamedt<exprt, L2> l2_arg = state.rename(code.operands()[i], ns);
     if(symex_config.simplify_opt)
     {
-      simplify_expr_with_value_sett simp{state.value_set, language_mode, ns};
+      simplify_expr_with_value_sett simp{
+        state.value_set, state.language_mode, ns};
       l2_arg.simplify(simp);
     }
     args.emplace_back(l2_arg);
   }
 
   const irep_idt output_id =
-    get_string_argument(id_arg, state.value_set, language_mode, ns);
+    get_string_argument(id_arg, state.value_set, state.language_mode, ns);
 
   target.output(state.guard.as_expr(), state.source, output_id, args);
 }
diff --git a/src/goto-symex/symex_clean_expr.cpp b/src/goto-symex/symex_clean_expr.cpp
index a650d97b707..b8a8d4180a7 100644
--- a/src/goto-symex/symex_clean_expr.cpp
+++ b/src/goto-symex/symex_clean_expr.cpp
@@ -127,7 +127,7 @@ void goto_symext::process_array_expr(statet &state, exprt &expr)
     ns,
     state.symbol_table,
     symex_dereference_state,
-    language_mode,
+    state.language_mode,
     false,
     log.get_message_handler());
 
@@ -187,7 +187,6 @@ void goto_symext::lift_let(statet &state, const let_exprt &let_expr)
     symex_targett::assignment_typet::HIDDEN,
     ns,
     symex_config,
-    language_mode,
     target}
     .assign_symbol(
       to_ssa_expr(state.rename<L1>(let_expr.symbol(), ns).get()),
diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp
index 69ff860f555..9f53513d2a9 100644
--- a/src/goto-symex/symex_dereference.cpp
+++ b/src/goto-symex/symex_dereference.cpp
@@ -220,7 +220,7 @@ goto_symext::cache_dereference(exprt &dereference_result, statet &state)
                              "symex",
                              "dereference_cache",
                              dereference_result.source_location(),
-                             language_mode,
+                             state.language_mode,
                              ns,
                              state.symbol_table)
                              .symbol_expr();
@@ -236,7 +236,6 @@ goto_symext::cache_dereference(exprt &dereference_result, statet &state)
     symex_targett::assignment_typet::STATE,
     ns,
     symex_config,
-    language_mode,
     target};
 
   assign.assign_symbol(
@@ -328,7 +327,7 @@ void goto_symext::dereference_rec(
       ns,
       state.symbol_table,
       symex_dereference_state,
-      language_mode,
+      state.language_mode,
       expr_is_not_null,
       log.get_message_handler());
 
diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp
index db4bfa133bc..6fdf9f4ff5e 100644
--- a/src/goto-symex/symex_function_call.cpp
+++ b/src/goto-symex/symex_function_call.cpp
@@ -131,13 +131,7 @@ void goto_symext::parameter_assignments(
 
       exprt::operandst lhs_conditions;
       symex_assignt{
-        shadow_memory,
-        state,
-        assignment_type,
-        ns,
-        symex_config,
-        language_mode,
-        target}
+        shadow_memory, state, assignment_type, ns, symex_config, target}
         .assign_rec(lhs, expr_skeletont{}, rhs, lhs_conditions);
     }
 
diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp
index ee725205ff3..6cb82a62d3b 100644
--- a/src/goto-symex/symex_goto.cpp
+++ b/src/goto-symex/symex_goto.cpp
@@ -75,7 +75,8 @@ void goto_symext::symex_goto(statet &state)
   renamedt<exprt, L2> renamed_guard = state.rename(std::move(new_guard), ns);
   if(symex_config.simplify_opt)
   {
-    simplify_expr_with_value_sett simp{state.value_set, language_mode, ns};
+    simplify_expr_with_value_sett simp{
+      state.value_set, state.language_mode, ns};
     renamed_guard.simplify(simp);
   }
   new_guard = renamed_guard.get();
diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp
index f287a070c89..7486f05949b 100644
--- a/src/goto-symex/symex_main.cpp
+++ b/src/goto-symex/symex_main.cpp
@@ -418,7 +418,7 @@ std::unique_ptr<goto_symext::statet> goto_symext::initialize_entry_point_state(
     symex_targett::sourcet(entry_point_id, start_function->body),
     symex_config.max_field_sensitivity_array_size,
     symex_config.simplify_opt,
-    language_mode,
+    ns.lookup(entry_point_id).mode,
     guard_manager,
     [storage](const irep_idt &id) { return storage->get_unique_l2_index(id); });
 
@@ -821,7 +821,7 @@ void goto_symext::try_filter_value_sets(
 
     const bool exclude_null_derefs = false;
     if(value_set_dereferencet::should_ignore_value(
-         value_set_element, exclude_null_derefs, language_mode))
+         value_set_element, exclude_null_derefs, state.language_mode))
     {
       continue;
     }
diff --git a/src/goto-symex/symex_start_thread.cpp b/src/goto-symex/symex_start_thread.cpp
index a394209c413..0681eb60413 100644
--- a/src/goto-symex/symex_start_thread.cpp
+++ b/src/goto-symex/symex_start_thread.cpp
@@ -99,7 +99,6 @@ void goto_symext::symex_start_thread(statet &state)
       symex_targett::assignment_typet::HIDDEN,
       ns,
       symex_config,
-      language_mode,
       target}
       .assign_symbol(lhs_l1, expr_skeletont{}, rhs, lhs_conditions);
     const exprt l2_lhs = state.rename(lhs_l1, ns).get();
@@ -151,7 +150,6 @@ void goto_symext::symex_start_thread(statet &state)
       symex_targett::assignment_typet::HIDDEN,
       ns,
       symex_config,
-      language_mode,
       target}
       .assign_symbol(lhs, expr_skeletont{}, rhs, lhs_conditions);
   }
diff --git a/unit/goto-symex/symex_assign.cpp b/unit/goto-symex/symex_assign.cpp
index c7785e0e693..934d0588fea 100644
--- a/unit/goto-symex/symex_assign.cpp
+++ b/unit/goto-symex/symex_assign.cpp
@@ -91,7 +91,6 @@ SCENARIO(
         symex_targett::assignment_typet::STATE,
         ns,
         symex_config,
-        irep_idt{},
         target_equation}
         .assign_symbol(ssa_foo, expr_skeletont{}, rhs1, guard);
       THEN("An equation is added to the target")
@@ -148,7 +147,6 @@ SCENARIO(
         symex_targett::assignment_typet::STATE,
         ns,
         symex_config,
-        irep_idt{},
         target_equation};
       symex_assign.assign_symbol(ssa_foo, expr_skeletont{}, rhs1, guard);
       THEN("An equation with an empty guard is added to the target")
@@ -235,7 +233,6 @@ SCENARIO(
         symex_targett::assignment_typet::STATE,
         ns,
         symex_config,
-        empty_language_mode,
         target_equation}
         .assign_symbol(struct1_ssa, skeleton, rhs, guard);
       THEN("Two equations are added to the target")

From 7ecf71adf30ea5bcb6b41b23ed43f63b3f2dd2ce Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 2 Dec 2025 02:00:23 +0000
Subject: [PATCH 06/14] Avoid invalid shift caused by excessive object bits

Use mp_integer to compute the number of permitted objects as the number
of object bits is related to the analysis target platform and need not
be within the analysis-execution platform's limits.
---
 .../smt2_incremental/convert_expr_to_smt.cpp       | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

diff --git a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp
index d5910628470..0af4c0f533a 100644
--- a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp
+++ b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp
@@ -877,21 +877,23 @@ static smt_termt convert_expr_to_smt(
     "Objects should be tracked before converting their address to SMT terms");
   const std::size_t object_id = object->second.unique_id;
   const std::size_t object_bits = config.bv_encoding.object_bits;
-  const std::size_t max_objects = std::size_t(1) << object_bits;
+  const mp_integer max_objects = power(2, object_bits);
   if(object_id >= max_objects)
   {
     throw analysis_exceptiont{
       "too many addressed objects: maximum number of objects is set to 2^n=" +
-      std::to_string(max_objects) + " (with n=" + std::to_string(object_bits) +
+      integer2string(max_objects) + " (with n=" + std::to_string(object_bits) +
       "); " +
       "use the `--object-bits n` option to increase the maximum number"};
   }
   const smt_termt object_bit_vector =
     smt_bit_vector_constant_termt{object_id, object_bits};
-  INVARIANT(
-    type->get_width() > object_bits,
-    "Pointer should be wider than object_bits in order to allow for offset "
-    "encoding.");
+  if(type->get_width() <= object_bits)
+  {
+    throw analysis_exceptiont{
+      "pointer should be wider than object_bits in order to allow for offset "
+      "encoding"};
+  }
   const size_t offset_bits = type->get_width() - object_bits;
   if(expr_try_dynamic_cast<symbol_exprt>(address_of.object()))
   {

From 1acc24e6fb15fc71e112079e0ebccfc005c956af Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 2 Dec 2025 11:07:02 +0000
Subject: [PATCH 07/14] DEBUG: add timing info to unit tests

---
 .github/workflows/clang-sanitizer.yaml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/.github/workflows/clang-sanitizer.yaml b/.github/workflows/clang-sanitizer.yaml
index 4622e867c3a..86d9c52f267 100644
--- a/.github/workflows/clang-sanitizer.yaml
+++ b/.github/workflows/clang-sanitizer.yaml
@@ -78,11 +78,11 @@ jobs:
         run: ccache -s
       - name: Run unit tests
         run: |
-          make -C unit test
-          make -C jbmc/unit test
+          make TAGS="-d yes" -C unit test
+          make TAGS="-d yes" -C jbmc/unit test
           echo "Running expected failure tests"
-          make TAGS="[!shouldfail]" -C unit test
-          make TAGS="[!shouldfail]" -C jbmc/unit test
+          make TAGS="-d yes [!shouldfail]" -C unit test
+          make TAGS="-d yes [!shouldfail]" -C jbmc/unit test
       - name: Run regression tests
         run: |
           export PATH=$PATH:`pwd`/src/solvers

From 188913a17559a999177bfb8babd50c91b7c5e199 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 2 Dec 2025 12:18:49 +0000
Subject: [PATCH 08/14] WIP: Debug unit test that does not terminate with
 sanitizer

---
 .github/workflows/clang-sanitizer.yaml | 2 +-
 unit/util/run.cpp                      | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/clang-sanitizer.yaml b/.github/workflows/clang-sanitizer.yaml
index 86d9c52f267..107794a2f18 100644
--- a/.github/workflows/clang-sanitizer.yaml
+++ b/.github/workflows/clang-sanitizer.yaml
@@ -78,7 +78,7 @@ jobs:
         run: ccache -s
       - name: Run unit tests
         run: |
-          make TAGS="-d yes" -C unit test
+          make TAGS="-d yes' '~[!shouldfail]' '~[not_ubsan]" -C unit test
           make TAGS="-d yes" -C jbmc/unit test
           echo "Running expected failure tests"
           make TAGS="-d yes [!shouldfail]" -C unit test
diff --git a/unit/util/run.cpp b/unit/util/run.cpp
index dc93a6e7cf8..09165f6231d 100644
--- a/unit/util/run.cpp
+++ b/unit/util/run.cpp
@@ -31,7 +31,7 @@ SCENARIO("shell_quote() escaping", "[core][util][run]")
 #endif
 }
 
-SCENARIO("run() error reporting", "[core][util][run]")
+SCENARIO("run() error reporting", "[core][util][run][not_ubsan]")
 {
   GIVEN("A command invoking a non-existent executable")
   {

From 8aa670e9585542e07828366f95fa1eaf172f85bd Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 2 Dec 2025 14:18:17 +0000
Subject: [PATCH 09/14] WIP: disable leak sanitizer to see what other problems
 we have

---
 .github/workflows/clang-sanitizer.yaml | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

diff --git a/.github/workflows/clang-sanitizer.yaml b/.github/workflows/clang-sanitizer.yaml
index 107794a2f18..df312da9c5d 100644
--- a/.github/workflows/clang-sanitizer.yaml
+++ b/.github/workflows/clang-sanitizer.yaml
@@ -16,11 +16,11 @@ jobs:
       CC: "ccache /usr/bin/clang"
       CXX: "ccache /usr/bin/clang++"
       # AddressSanitizer configuration for optimal CI performance
-      ASAN_OPTIONS: "abort_on_error=1:fast_unwind_on_malloc=0:detect_odr_violation=0:detect_leaks=1"
+      ASAN_OPTIONS: "abort_on_error=1:fast_unwind_on_malloc=0:detect_odr_violation=0:detect_leaks=0"
       # - `abort_on_error=1`: Terminate immediately on error
       # - `fast_unwind_on_malloc=0`: Use slower but more accurate stack unwinding
       # - `detect_odr_violation=0`: Disable One Definition Rule violation detection to reduce noise
-      # - `detect_leaks=1`: Enable leak detection
+      # - `detect_leaks=0`: Disable leak detection
       UBSAN_OPTIONS: "print_stacktrace=1:halt_on_error=1"
       # - `print_stacktrace=1`: Show stack traces for undefined behavior
       # - `halt_on_error=1`: Terminate on undefined behavior
@@ -58,15 +58,14 @@ jobs:
           echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
       - name: Zero ccache stats and limit in size
         run: ccache -z --max-size=500M
-      - name: Build with AddressSanitizer and LeakSanitizer
+      - name: Build with AddressSanitizer
         run: |
           # Build with sanitizers enabled - using -O1 for reasonable performance
           # -fsanitize=address: detects buffer overflows, use-after-free, etc.
-          # -fsanitize=leak: detects memory leaks
           # -fsanitize=undefined: detects undefined behavior
           # -fno-sanitize-recover=all: abort on first error for faster feedback
           # -g: include debug symbols for better error reporting
-          export SANITIZER_FLAGS="-fsanitize=address -fsanitize=leak -fsanitize=undefined -fno-sanitize-recover=all -g -O1"
+          export SANITIZER_FLAGS="-fsanitize=address -fsanitize=undefined -fno-sanitize-recover=all -g -O1"
           make -C src -j${{env.linux-vcpus}} \
             CXXFLAGS="$SANITIZER_FLAGS" \
             LINKFLAGS="$SANITIZER_FLAGS" \

From f68812e7808b8c81a3f24ccdb24dfc73bb6c5508 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 2 Dec 2025 15:57:42 +0000
Subject: [PATCH 10/14] fixup! Enable Clang sanitizers in Linux/Clang CI
 pipeline

---
 .github/workflows/clang-sanitizer.yaml | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/.github/workflows/clang-sanitizer.yaml b/.github/workflows/clang-sanitizer.yaml
index df312da9c5d..4409c5e8d49 100644
--- a/.github/workflows/clang-sanitizer.yaml
+++ b/.github/workflows/clang-sanitizer.yaml
@@ -73,6 +73,13 @@ jobs:
           make -C unit -j${{env.linux-vcpus}} \
             CXXFLAGS="$SANITIZER_FLAGS" \
             LINKFLAGS="$SANITIZER_FLAGS"
+          make -C jbmc/src -j${{env.linux-vcpus}} \
+            CXXFLAGS="$SANITIZER_FLAGS" \
+            LINKFLAGS="$SANITIZER_FLAGS" \
+            MINISAT2=../../minisat-2.2.1
+          make -C jbmc/unit -j${{env.linux-vcpus}} \
+            CXXFLAGS="$SANITIZER_FLAGS" \
+            LINKFLAGS="$SANITIZER_FLAGS"
       - name: Print ccache stats
         run: ccache -s
       - name: Run unit tests

From a2a63ba8bf97ae58d00e43d68bd1375ebb4c15f1 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 2 Dec 2025 16:32:47 +0000
Subject: [PATCH 11/14] fixup! DEBUG: add timing info to unit tests

---
 .github/workflows/clang-sanitizer.yaml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/clang-sanitizer.yaml b/.github/workflows/clang-sanitizer.yaml
index 4409c5e8d49..6fa997efb1a 100644
--- a/.github/workflows/clang-sanitizer.yaml
+++ b/.github/workflows/clang-sanitizer.yaml
@@ -87,8 +87,8 @@ jobs:
           make TAGS="-d yes' '~[!shouldfail]' '~[not_ubsan]" -C unit test
           make TAGS="-d yes" -C jbmc/unit test
           echo "Running expected failure tests"
-          make TAGS="-d yes [!shouldfail]" -C unit test
-          make TAGS="-d yes [!shouldfail]" -C jbmc/unit test
+          make TAGS="-d yes' '[!shouldfail]" -C unit test
+          make TAGS="-d yes' '[!shouldfail]" -C jbmc/unit test
       - name: Run regression tests
         run: |
           export PATH=$PATH:`pwd`/src/solvers

From 16d49c98e3003daffbed1684bf41d91f2617399a Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 2 Dec 2025 17:15:02 +0000
Subject: [PATCH 12/14] Add missing quotes

---
 jbmc/unit/Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/jbmc/unit/Makefile b/jbmc/unit/Makefile
index bc16c2ca851..592086d39c4 100644
--- a/jbmc/unit/Makefile
+++ b/jbmc/unit/Makefile
@@ -147,7 +147,7 @@ test: $(CATCH_TEST)
 	# Include hidden tests by specifying "*,[.]" for tests to count
 	if ! ./$(CATCH_TEST) "*,[.]" -l | grep -q "^$(N_CATCH_TESTS) matching test cases" ; then \
 	  ./$(CATCH_TEST) "*,[.]" -l ; fi
-	./$(CATCH_TEST) ${TAGS}
+	./$(CATCH_TEST) '${TAGS}'
 
 
 ###############################################################################

From ddbc14bbaf10dda0381d65bce3505c0def8ca21f Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 3 Dec 2025 14:21:47 +0000
Subject: [PATCH 13/14] Set pointer variable (TODO: refactor code)

---
 .../string_constraint_instantiation/instantiate_not_contains.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp b/jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp
index 34bcecc285f..08684c058b4 100644
--- a/jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp
+++ b/jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp
@@ -171,6 +171,7 @@ decision_proceduret::resultt check_sat(const exprt &expr, const namespacet &ns)
   bv_refinementt::infot info;
   info.ns = &ns;
   info.prop = &sat_check;
+  info.message_handler = &null_message_handler;
   info.output_xml = false;
   bv_refinementt solver(info);
   solver << expr;

From 3bb45cbf9d8a729f30eaa7f0ee8d76399e91d0c0 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 3 Dec 2025 18:09:04 +0000
Subject: [PATCH 14/14] Avoid undefined shift

---
 src/cprover/bv_pointers_wide.cpp | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/src/cprover/bv_pointers_wide.cpp b/src/cprover/bv_pointers_wide.cpp
index 9197306f0b1..ea2630d9d03 100644
--- a/src/cprover/bv_pointers_wide.cpp
+++ b/src/cprover/bv_pointers_wide.cpp
@@ -850,14 +850,16 @@ bvt bv_pointers_widet::add_addr(const exprt &expr)
 
   const pointer_typet type = pointer_type(expr.type());
   const std::size_t object_bits = get_object_width(type);
-  const std::size_t max_objects = std::size_t(1) << object_bits;
+  const mp_integer max_objects = power(2, object_bits);
 
-  if(a == max_objects)
+  if(a >= max_objects)
+  {
     throw analysis_exceptiont(
       "too many addressed objects: maximum number of objects is set to 2^n=" +
-      std::to_string(max_objects) + " (with n=" + std::to_string(object_bits) +
+      integer2string(max_objects) + " (with n=" + std::to_string(object_bits) +
       "); " +
       "use the `--object-bits n` option to increase the maximum number");
+  }
 
   return encode(a, type);
 }