Usage

As an illustrative example to show some of the ESBMC features concerning floating-point numbers, consider the following C code:

#include <assert.h>	
#include <math.h>
unsigned char nondet_uchar();
double nondet_double();
int main() {
unsigned char N = nondet_char();
double x = nondet_double();

if(x <= 0 || isnan(x))
  return 0;

unsigned short i = 0;

__VERIFIER_assume(x < 5);

double x_0 = x;  // Store initial value

__VERIFIER_assume(N >= 0 && N < 2);

// Loop invariant: 0 ≤ i ≤ N and x = x_0 * 2^i and x > 0
while(i < N) {
  __VERIFIER_assume(x > 0);
  __VERIFIER_assume(x == x_0 * pow(2, i));
  __VERIFIER_assume(0 <= i && i <= N);

  x = (2 * x);
  ++i;
}

assert(x > 0);
  return 0;
}

Here, ESBMC is invoked as follows: esbmc file.c --floatbv --k-induction where file.c is the C program to be checked, --floatbv indicates that ESBMC will use floating-point arithmetic to represent the program’s float and double variables, and --k-induction selects the k-induction proof rule. The user can select the SMT solver, property, and verification strategy. For this particular C program, ESBMC provides the following output as the verification result:

*** Checking inductive step
Starting Bounded Model Checking
Unwinding loop 2 iteration 1 file ex5.c line 8 function main
Not unwinding loop 2 iteration 2 file ex5.c line 8 function main
Symex completed in: 0.001s (40 assignments)
Slicing time: 0.000s (removed 16 assignments)
Generated 2 VCC(s), 2 remaining after simplification (24 assignments)
No solver specified; defaulting to Bitwuzla
Encoding remaining VCC(s) using bit-vector/floating-point arithmetic
Encoding to solver time: 0.005s
Solving with solver Bitwuzla
Encoding to solver time: 0.005s
Runtime decision procedure: 0.427s
BMC program time: 0.435s

VERIFICATION SUCCESSFUL

Solution found by the inductive step (k = 2)

As an illustrative example to show some of the ESBMC features concerning pointer safety, consider the following C code:

#include <stdlib.h>
int *a, *b;
int n;
#define BLOCK_SIZE 128
void foo () {
  int i;
  for (i = 0; i < n; i++)
    a[i] = -1;
  for (i = 0; i < BLOCK_SIZE - 1; i++)
    b[i] = -1;
}
int main () {
  n = BLOCK_SIZE;
  a = malloc (n * sizeof(*a));
  b = malloc (n * sizeof(*b));
  *b++ = 0;
  foo ();
  if (b[-1]) { free(a); free(b); }
  else { free(a); free(b); }
  return 0;
}

Here, ESBMC is invoked as follows:

esbmc file.c --memory-leak-check

where file.c is the C program to be checked and --memory-leak-check indicates that ESBMC will check for memory leaks. For this particular C program, ESBMC produces the following counterexample:

Counterexample:

State 1 file ex2.c line 14 function main thread 0
----------------------------------------------------
a = (signed int *)(&dynamic_1_array[0])

State 2 file ex2.c line 15 function main thread 0
----------------------------------------------------
b = (signed int *)0

State 3 file ex2.c line 16 function main thread 0
----------------------------------------------------
b = 0 + 1

State 6 file ex2.c line 16 function main thread 0
----------------------------------------------------
Violated property:
  file ex2.c line 16 function main
  dereference failure: NULL pointer

In the counterexample shown above, State 1 indicates that memory has been allocated, as indicated by ‘dynamic_1_array’. State 2 indicates that the malloc call failed and returned NULL, indicating that the memory was not allocated. Note that ESBMC allows the user to skip checking for malloc/new failures via --force-malloc-success. State 3 represents an assignment to pointer b. Lastly, State 6 reports a failure to dereference pointer b.

As an illustrative example to show some of the ESBMC features concerning concurrency, consider the following C code:

#include <assert.h>	
#include <pthread.h>
int n=0; //shared variable
pthread_mutex_t mutex;
void* P(void* arg) {
  int tmp, i=1;
  while (i<=10) {
    pthread_mutex_lock(&mutex);
    tmp = n;
    n = tmp + 1;
    pthread_mutex_unlock(&mutex);
    i++;
  }
  return NULL;
}
int main (void) {
  pthread_t id1, id2;
  pthread_mutex_init(&mutex, NULL);
  pthread_create(&id1, NULL, P, NULL);
  pthread_create(&id2, NULL, P, NULL);
  pthread_join(id1, NULL);
  pthread_join(id2, NULL);
  assert(n == 20);
}

Here, we create two threads id1 and id1; both threads will run the same code as implemented in P. Note that these two threads communicate via the shared memory n, which is protected by a mutex via pthread_mutex_lock and pthread_mutex_unlock. Note further that the thread main contains two joining points via pthread_join for id1 and id2.

ESBMC can be invoked as follows: esbmc file.c --context-bound 2 where file.c is the C program to be checked, and --context-bound nr limits the number of context switches for each thread. For this particular C program, ESBMC produces the following verification result:

*** Thread interleavings 612 ***
Unwinding loop 1 iteration 10 file test3.c line 6 function P
Unwinding loop 1 iteration 1 file test3.c line 6 function P
Unwinding loop 1 iteration 2 file test3.c line 6 function P
Unwinding loop 1 iteration 3 file test3.c line 6 function P
Unwinding loop 1 iteration 4 file test3.c line 6 function P
Unwinding loop 1 iteration 5 file test3.c line 6 function P
Unwinding loop 1 iteration 6 file test3.c line 6 function P
Unwinding loop 1 iteration 7 file test3.c line 6 function P
Unwinding loop 1 iteration 8 file test3.c line 6 function P
Unwinding loop 1 iteration 9 file test3.c line 6 function P
Unwinding loop 1 iteration 10 file test3.c line 6 function P
Symex completed in: 0.031s (431 assignments)
Slicing time: 0.001s (removed 183 assignments)
Generated 149 VCC(s), 7 remaining after simplification (248 assignments)
No solver specified; defaulting to Bitwuzla
Encoding remaining VCC(s) using bit-vector/floating-point arithmetic
Encoding to solver time: 0.004s
Solving with solver Bitwuzla
Encoding to solver time: 0.004s
Runtime decision procedure: 0.001s
BMC program time: 0.040s

VERIFICATION SUCCESSFUL

Verifying Python Programs

ESBMC has a dedicated Python frontend. See the Python section for how to verify Python programs, the supported features, and worked examples.

Witness Generation

When ESBMC refutes a property, it produces a counterexample that can be used to debug the program to find the root cause of the problem. For this purpose, ESBMC can produce the counterexample in graphml format to make its evaluation easier (e.g., by building a tool that allows graphical visualization).

As an illustrative example, consider the following fragment of C code, where we declare two bit-vectors of size 10 each: x and y, and then check whether x == y.

#include <assert.h>

int main() {
  _ExtInt(10) x = nondet_float();
  _ExtInt(10) y = nondet_int();
  assert(x == y);
  return 0;
}

If we call ESBMC as esbmc main.c --witness-output main.graphml, where main.c is the C program we want to verify, while main.graphml stores the counterexample in graphml format, then ESBMC will produce the following output:

esbmc main.c --witness-output main.graphml

<?xml version="1.0" encoding="utf-8"?>
<graphml xmlns="http://graphml.graphdrawing.org/xmlns" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance">
  <key id="frontier" attr.name="isFrontierNode" attr.type="boolean" for="node">
    <default>false</default>
  </key>
  <key id="violation" attr.name="isViolationNode" attr.type="boolean" for="node">
    <default>false</default>
  </key>
  <key id="entry" attr.name="isEntryNode" attr.type="boolean" for="node">
    <default>false</default>
  </key>
  <key id="sink" attr.name="isSinkNode" attr.type="boolean" for="node">
    <default>false</default>
  </key>
  <key id="cyclehead" attr.name="cyclehead" attr.type="boolean" for="node">
    <default>false</default>
  </key>
  <key id="sourcecodelang" attr.name="sourcecodeLanguage" attr.type="string" for="graph"/>
  <key id="programfile" attr.name="programfile" attr.type="string" for="graph"/>
  <key id="programhash" attr.name="programhash" attr.type="string" for="graph"/>
  <key id="creationtime" attr.name="creationtime" attr.type="string" for="graph"/>
  <key id="specification" attr.name="specification" attr.type="string" for="graph"/>
  <key id="architecture" attr.name="architecture" attr.type="string" for="graph"/>
  <key id="producer" attr.name="producer" attr.type="string" for="graph"/>
  <key id="sourcecode" attr.name="sourcecode" attr.type="string" for="edge"/>
  <key id="startline" attr.name="startline" attr.type="int" for="edge"/>
  <key id="startoffset" attr.name="startoffset" attr.type="int" for="edge"/>
  <key id="control" attr.name="control" attr.type="string" for="edge"/>
  <key id="invariant" attr.name="invariant" attr.type="string" for="node"/>
  <key id="invariant.scope" attr.name="invariant.scope" attr.type="string" for="node"/>
  <key id="assumption" attr.name="assumption" attr.type="string" for="edge"/>
  <key id="assumption.scope" attr.name="assumption" attr.type="string" for="edge"/>
  <key id="assumption.resultfunction" attr.name="assumption.resultfunction" attr.type="string" for="edge"/>
  <key id="enterFunction" attr.name="enterFunction" attr.type="string" for="edge"/>
  <key id="returnFromFunction" attr.name="returnFromFunction" attr.type="string" for="edge"/>
  <key id="endline" attr.name="endline" attr.type="int" for="edge"/>
  <key id="endoffset" attr.name="endoffset" attr.type="int" for="edge"/>
  <key id="threadId" attr.name="threadId" attr.type="string" for="edge"/>
  <key id="createThread" attr.name="createThread" attr.type="string" for="edge"/>
  <key id="witness-type" attr.name="witness-type" attr.type="string" for="graph"/>
  <graph edgedefault="directed">
    <data key="producer">ESBMC 6.7.0</data>
    <data key="sourcecodelang">C</data>
    <data key="architecture">64bit</data>
    <data key="programfile">main.c</data>
    <data key="programhash">7ba149c407ef7ae9e971bbc937b37a624575d6a5</data>
    <data key="specification">CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )</data>
    <data key="creationtime">2021-06-07T13:37:38</data>
    <data key="witness-type">violation_witness</data>
    <node id="N0">
      <data key="entry">true</data>
    </node>
    <node id="N1"/>
    <edge id="E0" source="N0" target="N1">
      <data key="enterFunction">main</data>
      <data key="createThread">0</data>
    </edge>
    <node id="N2"/>
    <edge id="E1" source="N1" target="N2">
      <data key="startline">4</data>
      <data key="assumption">x = -512;</data>
      <data key="threadId">0</data>
    </edge>
    <node id="N3"/>
    <edge id="E2" source="N2" target="N3">
      <data key="startline">5</data>
      <data key="assumption">y = -166;</data>
      <data key="threadId">0</data>
    </edge>
    <node id="N4">
      <data key="violation">true</data>
    </node>
    <edge id="E3" source="N3" target="N4">
      <data key="startline">93</data>
      <data key="threadId">0</data>
    </edge>
  </graph>
</graphml>

We recommend reading Exchange Format for Violation Witnesses and Correctness Witnesses to obtain further information about violation and correctness witnesses in graphml format.

A GraphML trace step that comes from a header or from one of ESBMC’s operational models is emitted with an originfile naming the file it came from, and keeps that file’s own line numbers instead of having them resolved against the verified file. originfile is not a key the exchange format defines, so a conforming validator ignores it; the edges it appears on were unmatchable to a validator before, either way. YAML witnesses have no equivalent, so there a waypoint is hoisted to its innermost call site inside an input file and one that cannot name an input file is dropped, as README-YAML.md requires.

Unwinding Assertions

In ESBMC, all loops are “unwound”, i.e., replaced by several guarded copies of the loop body; the same happens for backward “gotos” and recursive functions. Soundness requires that ESBMC insert a so-called unwinding assertion at the end of the loop. As an example, consider the simple C code fragment illustrated below:

unsigned int x=∗;
while ( x>0) x−−;
assert ( x==0);

Note that the loop in line 2 runs an unknown number of times, depending on the initial non-deterministic value assigned to x in line 1. The assertion in line 3 holds independently of x’s initial value. BMC tools typically fail to verify programs that contain such loops. In particular, BMC tools introduce an unwinding assertion at the end of the loop, as illustrated in line 5 of this C code fragment.

unsigned int x=∗;
if(x>0)
  x−−;   // k copies
  ...
assert (!(x>0));
assert(x==0);

This unwinding assertion in line 5 causes the BMC tool to fail if k is too small, as follows:

#include <assert.h>
unsigned int nondet_uint();
int main() {
  unsigned int x=nondet_uint();
  while(x>0) x--;

  assert(x==0);
  return 0;
}

esbmc file.c --unwind 3

Counterexample:

State 1 file file.c line 4 function main thread 0
----------------------------------------------------
x = 3170305 (00000000 00110000 01100000 00000001)

State 2 file file.c line 5 function main thread 0
----------------------------------------------------
x = 3170304 (00000000 00110000 01100000 00000000)

State 3 file file.c line 5 function main thread 0
----------------------------------------------------
x = 3170303 (00000000 00110000 01011111 11111111)

State 4 file file.c line 5 function main thread 0
----------------------------------------------------
Violated property:
file file.c line 5 function main
unwinding assertion loop

--no-unwinding-assertions removes that assertion, so paths past the bound are assumed away rather than reported. A proof obtained that way holds only up to the bound, and a run whose loops were cut short says so above the verdict:

** 0 of 1 properties failed, 1 passed
WARNING: the unwinding bound cut a loop short while unwinding checks were
disabled, so paths past the bound were assumed away rather than verified; this
result holds only up to that bound

VERIFICATION SUCCESSFUL

Verification Strategies

ESBMC offers several incremental strategies that control how loops are unwound and whether correctness can be proven. For an in-depth explanation of how each algorithm works, see Verification Algorithms.

--max-k-step N caps the unwind bound (default 50); --k-step N changes the increment granularity.

Reusing common subexpressions

--gcse precomputes a subexpression shared between assignments into an intermediate variable, so symbolic execution builds it once rather than at every use. Whether a rewrite is safe depends on what the program’s pointers can address, which comes from an inclusion-based (Andersen) whole-program points-to analysis over the GOTO program. The analysis is deliberately imprecise — symbolic execution supplies the real precision — and abstains on any expression whose targets it cannot determine, in which case the rewrite is not made. The flag is off by default.

Selecting the floating-point rounding mode

Under --floatbv, every floating-point operation reads its rounding mode from the global __ESBMC_rounding_mode, which starts at round-to-nearest-even. Five flags change that initial value:

esbmc file.c --floatbv --round-to-zero

Only the initial value is rewritten, so a program calling fesetround() still changes the mode from that point on.

Function-pointer calls with no target

A call through a function pointer whose value matches no function in the program is, by default, assumed to reach some external definition, so ESBMC keeps the path alive. --closed-world-fnptr instead treats such a call as unreachable:

esbmc file.c --closed-world-fnptr

Use it when the program under verification is the whole program — no dynamic loading, no linker-supplied implementations — so a pointer with no compatible target genuinely cannot be called. It is off by default because assuming the world is closed can prune real behaviour when it is not.

Verifying modules that span multiple files

ESBMC can verify code that relies on existing infrastructure. Consider a program whose mul function lives in a separate library:

#include "lib.h"
// Running with: esbmc --overflow-check main.c lib.c
int main() {
  int64_t a, b, r;
  if (mul(a, b, &r)) {
    __ESBMC_assert(r == a * b, "Expected result from multiplication");
  }
  return 0;
}

Invoke ESBMC with the include path and the implementation file:

esbmc main.c --overflow-check -I lib/ lib/lib.c

where --overflow-check enables arithmetic over-/underflow checks and -I path sets the include path. The library under lib/ is:

// lib.h
#include <stdint.h>
_Bool mul(const int64_t a, const int64_t b, int64_t *res);

// lib.c
#include "lib.h"
_Bool mul(int64_t a, int64_t b, int64_t *res) {
  if ((a == 0) || (b == 0)) { *res = 0; return 1; }
  else if (a == 1)          { *res = b; return 1; }
  else if (b == 1)          { *res = a; return 1; }
  *res = a * b;   // there exists an overflow
  return 1;
}

ESBMC reports the overflow at the unguarded multiplication:

Counterexample:

State 1 file lib.c line 14 function mul thread 0
----------------------------------------------------
Violated property:
file lib.c line 14 function mul
arithmetic overflow on mul
!overflow("*", a, b)

VERIFICATION FAILED

Checking restrict pointer aliasing

The C restrict qualifier is a promise to the compiler that, for the lifetime of the pointer, the object it points to is accessed only through that pointer. Calling a function with two restrict parameters that alias the same object — when at least one access is a write — is undefined behaviour (C11 6.7.3.1). Compilers exploit this promise to optimise, so a violation can silently miscompile.

The opt-in --restrict-check flag turns that contract into a checkable property. At the entry of every function with two or more restrict-qualified pointer parameters, ESBMC asserts that their pointed-to element footprints (sizeof(*p) bytes each) do not overlap within a shared object:

void f(int *restrict a, int *restrict b) {
  *a = 1;
  *b = 2;
}

int main(void) {
  int x = 0;
  f(&x, &x);   // a and b alias the same object
  return 0;
}

esbmc file.c --restrict-check

ESBMC reports the aliasing at the function entry:

[Counterexample]

State 1 file file.c line 2 column 3 function f thread 0
----------------------------------------------------
Violated property:
  file file.c line 2 column 3 function f
  restrict pointer aliasing
  !(a != 0 && b != 0 && SAME-OBJECT(a, b) && POINTER_OFFSET(a) < POINTER_OFFSET(b) + 4 && POINTER_OFFSET(b) < POINTER_OFFSET(a) + 4)

VERIFICATION FAILED

The footprint is an under-approximation of the accessed region, so two pointers into the same object whose element ranges are genuinely disjoint are never flagged — f(&arr[0], &arr[2]) verifies successfully. Null parameters designate no object and are exempt.

The check is off by default; without --restrict-check the program above verifies successfully. Its scope and known limitations:

• Only function-parameter aliasing is checked; there is no whole-program “based-on” tracking of derived pointers.
• It over-approximates the modification clause of 6.7.3.1p4: the assertion fires on overlap regardless of whether the body performs a modifying access, and const-qualified targets are not exempt (a const access path is still undefined once the shared object is modified by any means).

Assuming the contract instead of checking it

--restrict-assume is the dual of --restrict-check: instead of asserting the contract, it assumes the entry function’s restrict pointer parameters do not alias. Use it when verifying a function in isolation, where non-aliasing is a precondition the callers must honour rather than something the function can establish:

esbmc file.c --function f --restrict-assume

The assumption is scoped to the entry point only, and it does not imply the parameters are distinct pointers: f(NULL, NULL) is a conforming call (C11 6.7.3.1p4), so a != b still does not follow.

Per-property results

Every verification run ends with a ** Results: block naming each property, grouped by file and function in source order. It is printed whatever the strategy — plain BMC, --incremental-bmc, --k-induction — and --result-only keeps it while suppressing the rest of the output (a coverage run reports its own goals instead):

esbmc file.c --result-only

** Results:
file.c, function main
  PASSED       [main.assertion.1]  line 5  A1
  FAILED       [main.assertion.2]  line 6  A2

** 1 of 2 properties failed, 1 passed

VERIFICATION FAILED

A property is reported NOT CHECKED rather than PASSED when the run never separated it. A default run stops at the first violation, so the properties after it were never decided, and saying they passed would be wrong:

  PASSED       [main.assertion.1]  line 5  addition commutes
  FAILED       [main.assertion.2]  line 8  a is not one
  NOT CHECKED  [main.assertion.3]  line 9  a is not two

** 1 of 3 properties failed, 1 passed, 1 not checked
   (this mode stops at the first violation; use --multi-property for a verdict on every property)

Adding --multi-property decides all three, and appends the solver and its decision-procedure time to the summary.

Bounding the stack

esbmc file.c --stack-limit 8192
esbmc file.c --total-stack-limit 65536

--stack-limit bounds a single stack frame, so a deep recursion whose individual frames each fit never trips it. --total-stack-limit bounds the combined size of all live frames instead, which is what a real stack budget constrains. ESBMC’s own operational models are excluded from the total, so the bound stays calibratable against the program’s own frames.

Both bounds are given in bits, not bytes. The total is accounted per symbolic path at declaration points, and over-approximates for spawned threads. A violation names the declaration that crossed the bound:

Total stack limit property was violated when declaring buf

Multiple Property Verification

esbmc file.c --multi-property

ESBMC can verify the satisfiability of all claims of a given bound. In multi-property mode, ESBMC does not stop at the first counterexample; it continues until all bugs are found. Relevant options:

• --multi-property — verify all claims of the current bound (also activates --no-remove-unreachable).
• --multi-fail-fast N — stop after the first N violations.
• --multi-property-interleavings N — for concurrent programs, keep exploring thread interleavings after a violation until N consecutive ones reach a verdict on no new property (default 100, must be positive).
• --keep-verified-claims — do not skip verified claims (assertions inside a loop body are then re-verified during unwinding).
• --all-witnesses — after a property is violated, enumerate further inputs that also violate it (implies --multi-property; see below).
• --max-witnesses N — cap witnesses per property (default 16; 0 = unlimited).
• --full-traces — print every trace state per witness instead of the 50 nearest the failure (only meaningful with --all-witnesses).

A claim the solver never decided — an error, or a formula handed off without an answer under --smt-formula-only — is no longer folded into VERIFICATION SUCCESSFUL; a solver error additionally names the claim it failed on.

Verdicts accumulate across the whole run and each property is reported exactly once at the end, with failed dominating unknown dominating passed — so a property discharged under one schedule and violated under another is reported as violated rather than printing contradictory lines. For a concurrent program, exploration continues past the first violation until --multi-property-interleavings consecutive interleavings decide nothing new; a run that stops early states that its report is partial.

Enumerating all violating inputs

esbmc file.c --all-witnesses
esbmc file.c --all-witnesses --max-witnesses 4

By default --multi-property reports a single counterexample per failing property. --all-witnesses instead enumerates distinct concrete input vectors that violate the same property, until the set is exhausted (UNSAT) or the --max-witnesses cap is reached — useful for fault localisation, test-case mining, and characterising the failing-input sub-domain.

#include <assert.h>
int main(void) {
  int x;                 // nondet
  if (x > 0) x--; else x++;
  assert(x != 0);        // violated by x == 1 AND x == -1
  return 0;
}

esbmc file.c --all-witnesses reports both witnesses:

[Counterexamples - 2 witnesses]

  Inputs by witness:
    #1 : [0] = -1
    #2 : [0] = 1

  ┌─ Witness 1 of 2 ─────────────────────────────
  │  Inputs : [0] = -1
  │  Trace  :
  │    ...
  └──────────────────────────────────────────────

  ┌─ Witness 2 of 2 ─────────────────────────────
  │  Inputs : [0] = 1
  │  Trace  :
  │    ...
  └──────────────────────────────────────────────

Summary: 2 distinct input tuples violate this property (enumeration stopped: UNSAT after 2 witnesses)

Internally the same SMT instance is re-solved with a blocking clause over the nondet input symbols, so enumerating N witnesses is much cheaper than running ESBMC N times. Floating-point inputs are handled specially (the NaN equivalence class is excluded as a whole; other values use bit-pattern equality, so +0 and -0 are distinct). The footer states why enumeration stopped; only UNSAT after N means the witness set is complete.

Implementation notes. Blocking clauses are scoped to a single SMT context frame (push_ctx/pop_ctx) per claim, so the feature is safe under --smt-during-symex and does not leak between claims. Machine-readable artifacts (--cex-output, --generate-testcase, --generate-html-report, --generate-json-report, --witness-output-graphml, --witness-output-yaml) fan out per witness using the <phase>-k<K>-<N>-<file> prefix scheme — <phase> is the verification phase (base/fwd/indstep/bmc), <K> the unwind bound, and <N> a decimal increasing from zero — one file per witness, so it is also safe under --parallel-solving, and counterexamples found in different k-induction phases or k-steps do not overwrite each other. Enumeration is skipped during the inductive step of k-induction (a SAT result there means UNKNOWN, not a real counterexample).

Reading a multi-witness report. Every witness’s inputs are collected in the Inputs by witness: block under the header, before the first trace, since that is what differs between them; if the list was cut short by --max-witnesses, the header says so rather than leaving it to the footer. Each trace is then truncated to the 50 states nearest the failure, with a count of what was dropped — pass --full-traces for the whole trace. If you only need the violating inputs, that first block is usually enough, and the machine-readable per-witness files give the full data without the noise.

Formally this is bounded projected model enumeration for a fixed property: the blocking-clause loop from SAT all-solutions algorithms, lifted to SMT and projected onto the nondet input symbols. See McMillan, Applying SAT Methods in Unbounded Symbolic Model Checking, CAV 2002 (doi), and Grumberg, Schuster, Yadgar, Memory Efficient All-Solutions SAT Solver and Its Application for Reachability Analysis, FMCAD 2004 (doi). It complements dynamic-symbolic-execution test generation (KLEE, DART, SAGE), which varies the path condition to maximise coverage; --all-witnesses instead fixes the failure path and enumerates input vectors on it.

Suppressing assertions inside the operational models

esbmc file.c --no-library-assertions

ESBMC’s operational models assert their own API preconditions (for example "Sem is not initialized"). --no-library-assertions drops those claims while keeping every assertion in the program under verification — useful when a model precondition is deliberately violated in code you do not own.

It hides genuine API misuse the models report, so it is off by default. It also leaves the checks ESBMC generates inside model code (those are controlled by --no-standard-checks), renumbers --claim indices, and is unsupported for Python.

When ESBMC itself crashes

A SIGSEGV or SIGBUS inside ESBMC is an internal error, not a verification result, and is reported as one rather than leaving the exit status as its only trace:

ESBMC caught SIGSEGV: this is an internal error, not a verification result.
Re-run with --segfault-handler for a backtrace.
Please report it at https://github.com/esbmc/esbmc/issues

The report needs no flag and runs on an alternate signal stack, so a crash from stack exhaustion is reported too. A handler installed by someone else is left alone, so an AddressSanitizer build keeps its own richer report. --segfault-handler replaces this reporter with one that prints a backtrace and the process memory map, and covers SIGABRT as well — asking for the backtrace is explicit intent, so that one does not defer to a foreign handler.

Supported SMT backends

ESBMC integrates several SMT solvers directly via their APIs, and on Unix can also drive an external solver process, either interactively over a pipe or in one-shot batch mode:

Bitwuzllob and NeuroSym are one-shot subprocess backends: ESBMC renders the formula to an SMT-LIB2 file and runs an external program on it in batch mode — mallob in mono mode (Bitwuzla on the massively parallel Mallob platform) for Bitwuzllob, and the NeuroSym neural-guided solver (GAN with Z3 fallback, QF_BV only) for NeuroSym. The external command is set with --bitwuzllob-prog CMD / --neurosym-prog CMD (every %f is replaced by the formula file), and counterexamples are reconstructed by a local interactive SMT-LIB2 solver given via --bitwuzllob-model-prog CMD / --neurosym-model-prog CMD (e.g. "z3 -in"). Neither backend is ever picked implicitly, and NeuroSym rejects --ir and incremental strategies.

Floating-point arithmetic is encoded with the SMT floating-point theory (fp.add, fp.lt, …) on every backend that offers it — Bitwuzla, Z3, MathSAT, CVC4/CVC5 — and lowered to bit-vectors elsewhere. --fp2bv forces the bit-vector lowering on any backend, which is the encoding to reach for when a property depends on the sign of a NaN: the theory cannot represent it (#7021). fmod, remainder and remquo are always lowered through a bit-vector round-trip, since the theory’s fp.rem is far slower to solve.

An alternative default solver can be set with --default-solver SOLVER (the name without the --), which suits a shell alias or the ESBMC_OPTS environment variable. The CMD for the SMTLIB backend is interpreted by the shell, so it can include options or chain commands (the tools must be on PATH):

• boolector --incremental
• z3 -in
• tee formula.smt2 | z3 -in | tee output.txt
• yices-smt2 --incremental
• cvc5 -L smt2 -m

Remember to quote the CMD string when invoking ESBMC.

A backend that cannot decide a goal says so rather than ending the run without a verdict. Under the integer/real encoding (--ir, --ir-ieee) Z3’s smt tactic is incomplete for nonlinear real arithmetic, so the tactic chain falls back to qfnra-nlsat on exactly the goals smt abandoned, and declines anything outside QF_NRA. Bitwuzla returns a query term unchanged when evaluating it would need a quantifier it never registered; that is reported as an unknown value, as the Z3 backend already did.

Symmetry breaking

Symmetric formulas — most often a running maximum or minimum folded over an uninitialised array — make the backend solver enumerate equivalent case splits. ESBMC recognises those max/min folds and asserts the redundant bounds they imply before solving, which cuts the search. This is on by default; pass --no-symmetry-breaking to disable it if the extra constraints hurt on a particular benchmark.