# With Clang 13.0.0
$ cabal run exe:crux-llvm -- test.c -O0
[Crux] Using pointer width: 64 for file crux-build/crux~test.bc
[Crux] Simulating function main
[Crux] All goals discharged through internal simplification.
[Crux] Overall status: Valid.

# With Clang 14.0.0
$ cabal run exe:crux-llvm -- test.c -O0
[Crux] Using pointer width: 64 for file crux-build/crux~test.bc
[Crux] Simulating function main
[Crux] Attempting to prove verification conditions.
[Crux] *** debug executable: results/test/debug-2
[Crux] *** break on line: 2
[Crux] Found counterexample for verification goal
[Crux]   test.c:2:16: error: in fmuladd
[Crux]   Failed to load function handle
[Crux]   Details:
[Crux]     No implementation or override found for pointer
[Crux]     The given pointer could not be resolved to a callable function
[Crux]     No implementation or override found for pointer
[Crux]     Attempting to load callable function with type: double(double, double, double)
[Crux]       Via pointer: Global symbol "llvm.fmuladd.f64" (2, 0x0:[64])
[Crux]     In memory state:
[Crux]       Stack frame fmuladd
[Crux]         Allocations:
[Crux]           StackAlloc 9 0x8:[64] Mutable 8-byte-aligned test.c:1:43
[Crux]           StackAlloc 8 0x8:[64] Mutable 8-byte-aligned test.c:1:33
[Crux]           StackAlloc 7 0x8:[64] Mutable 8-byte-aligned test.c:1:23
[Crux]         Writes:
[Crux]           Indexed chunk:
[Crux]             7 |->   *(7, 0x0:[64]) := 1
[Crux]             8 |->   *(8, 0x0:[64]) := 2
[Crux]             9 |->   *(9, 0x0:[64]) := 3
[Crux]       Stack frame main
[Crux]         Allocations:
[Crux]           StackAlloc 6 0x8:[64] Mutable 8-byte-aligned test.c:6:10
[Crux]           StackAlloc 5 0x4:[64] Mutable 4-byte-aligned internal
[Crux]         Writes:
[Crux]           Indexed chunk:
[Crux]             5 |->   memset (5, 0x0:[64]) 0x0:[8] 0x4:[64]
[Crux]       Base memory
[Crux]         Allocations:
[Crux]           GlobalAlloc 4 0x0:[64] Immutable 1-byte-aligned [defined function ] main
[Crux]           GlobalAlloc 3 0x0:[64] Immutable 1-byte-aligned [defined function ] fmuladd
[Crux]           GlobalAlloc 2 0x0:[64] Immutable 1-byte-aligned [external function] llvm.fmuladd.f64
[Crux]           GlobalAlloc 1 0x0:[64] Immutable 1-byte-aligned [external function] llvm.dbg.declare
[Crux]     in context:
[Crux]       fmuladd
[Crux]       main
[Crux] Goal status:
[Crux]   Total: 1
[Crux]   Proved: 0
[Crux]   Disproved: 1
[Crux]   Incomplete: 0
[Crux]   Unknown: 0
[Crux] Overall status: Invalid.