To generate and use a counterexample harness follow the following steps

  > sea pf -m64 in.c --cex=harness.ll
  > sea exe -m64 -g in.c harness.ll -o out
  > ./out
  __VERIFIER_error was executed

Option `-m64' is necessary on 64-bit platforms because the run-time
library is compiled under host architecture, but sea-clang defaults to
`-m32'.

The resulting binary `out` can be debugged with gdb, lldb, and valgrind.

The default implementation does not allocate memory for external
addresses which are dereferenced during the execution of the
counterexample. Instead, it returns some default value each time an
external address is read. Although very simple, this approach does not
always succeeds. 

In cases, where the above commands do not generate a counterexample
harness that triggers the error location (i.e.,`__VERIFIER_error was
executed` is not printed), try:


  > sea pf -m64 --bv-cex --horn-bv-part-mem in.c --cex=harness.ll
  > sea exe -m64 -g --alloc-mem in.c harness.ll -o out
  > ./out
  __VERIFIER_error was executed
  
  
The options `--bv-cex --horn-bv-part-mem` makes sure that SeaHorn
models the potential counterexample generated by the back-end solvers
using bit-level precision. In addition, it ensures that all memory
regions are disjoint from each other, memory addresses are aligned,
etc. The option `--alloc-mem` allocates on-the-fly physical memory for
external memory.
