ex3-undef.good

[Crux] Using pointer width: 64 for file crux-build/crux~ex3-undef.bc
[Crux] Simulating function "main"
[Crux] Attempting to prove verification conditions.
[Crux] Counter example for test-data/golden/ex3-undef.c:11:9: error: in generate_value
Failed to load function handle
Details:
  No implementation or override found for pointer: "update_value"
[Crux] Failed to build counterexample executable
`clang` compilation failed.
*** Exit code: 1
*** Standard out:
*** Standard error:
   In file included from results/ex3-undef/counter-example-11.c:1:
   In file included from /nix/store/qsq3wklnkdy4hj17d055slsqhxc7mwxw-clang-wrapper-9.0.1/resource-root/include/stdint.h:52:
   In file included from /nix/store/z7zadp87kxyrpi0x7mwwz3fxv27g9k76-glibc-2.32-35-dev/include/stdint.h:26:
   In file included from /nix/store/z7zadp87kxyrpi0x7mwwz3fxv27g9k76-glibc-2.32-35-dev/include/bits/libc-header-start.h:33:
   /nix/store/z7zadp87kxyrpi0x7mwwz3fxv27g9k76-glibc-2.32-35-dev/include/features.h:397:4: warning: _FORTIFY_SOURCE requires compiling with optimization (-O) [-W#warnings]
   #  warning _FORTIFY_SOURCE requires compiling with optimization (-O)
      ^
   1 warning generated.
   In file included from /home/kquick/work/Polyglot/crucible-polyglot2-darcsClean/crux-llvm/././c-src/concrete-backend.c:1:
   In file included from /nix/store/z7zadp87kxyrpi0x7mwwz3fxv27g9k76-glibc-2.32-35-dev/include/stdio.h:27:
   In file included from /nix/store/z7zadp87kxyrpi0x7mwwz3fxv27g9k76-glibc-2.32-35-dev/include/bits/libc-header-start.h:33:
   /nix/store/z7zadp87kxyrpi0x7mwwz3fxv27g9k76-glibc-2.32-35-dev/include/features.h:397:4: warning: _FORTIFY_SOURCE requires compiling with optimization (-O) [-W#warnings]
   #  warning _FORTIFY_SOURCE requires compiling with optimization (-O)
      ^
   1 warning generated.
   In file included from test-data/golden/ex3-undef.c:1:
   In file included from /nix/store/z7zadp87kxyrpi0x7mwwz3fxv27g9k76-glibc-2.32-35-dev/include/stdio.h:27:
   In file included from /nix/store/z7zadp87kxyrpi0x7mwwz3fxv27g9k76-glibc-2.32-35-dev/include/bits/libc-header-start.h:33:
   /nix/store/z7zadp87kxyrpi0x7mwwz3fxv27g9k76-glibc-2.32-35-dev/include/features.h:397:4: warning: _FORTIFY_SOURCE requires compiling with optimization (-O) [-W#warnings]
   #  warning _FORTIFY_SOURCE requires compiling with optimization (-O)
      ^
   1 warning generated.
   /nix/store/rqfgki7ck1bxqhk3hd7wziqhahjadfbj-binutils-2.35.1/bin/ld: /tmp/nix-shell.htRLyY/ex3-undef-dbf3f5.o: in function `generate_value':
   /home/kquick/work/Polyglot/crucible-polyglot2-darcsClean/crux-llvm/test-data/golden/ex3-undef.c:11: undefined reference to `update_value'
   clang-9: error: linker command failed with exit code 1 (use -v to see invocation)


[Crux] Found counterexample for verification goal
test-data/golden/ex3-undef.c:11:9: error: in generate_value
Failed to load function handle
Details:
  No implementation or override found for pointer: "update_value"
  The given pointer could not be resolved to a callable function
  No implementation or override found for pointer: "update_value"
  Attempting to load callable function with type: i8(i8, i8)
    Via pointer: Global symbol "update_value" (2, 0x0:[64])
  In memory state:
    Stack frame generate_value
      No writes or allocations
    Stack frame get_value
      No writes or allocations
    Stack frame main
      No writes or allocations
    Base memory
      Allocations:
        GlobalAlloc 10 0x1d:[64] Immutable 1-byte-aligned [global variable  ] .str.1
        GlobalAlloc 9 0x5:[64] Immutable 1-byte-aligned [global variable  ] .str
        GlobalAlloc 8 0x0:[64] Immutable 1-byte-aligned [defined function ] main
        GlobalAlloc 7 0x0:[64] Immutable 1-byte-aligned [defined function ] get_value
        GlobalAlloc 6 0x0:[64] Immutable 1-byte-aligned [defined function ] generate_value
        GlobalAlloc 5 0x0:[64] Immutable 1-byte-aligned [external function] crucible_assert
        GlobalAlloc 4 0x0:[64] Immutable 1-byte-aligned [external function] crucible_assume
        GlobalAlloc 3 0x0:[64] Immutable 1-byte-aligned [external function] crucible_int8_t
        GlobalAlloc 2 0x0:[64] Immutable 1-byte-aligned [external function] update_value
        GlobalAlloc 1 0x0:[64] Immutable 1-byte-aligned [external function] llvm.dbg.value
      Writes:
        Indexed chunk:
          9 |->   *(9, 0x0:[64]) := "seed\NUL"
          10 |->   *(10, 0x0:[64]) := "test-data/golden/ex3-undef.c\NUL"
[Crux] Goal status:
[Crux]   Total: 1
[Crux]   Proved: 0
[Crux]   Disproved: 1
[Crux]   Incomplete: 0
[Crux]   Unknown: 0
[Crux] Overall status: Invalid.

ex3-undef.z3.out

[Crux] Using pointer width: 64 for file crux-build/crux~ex3-undef.bc
[Crux] Simulating function "main"
[Crux] Could not locate named function: update_value
Called at: test-data/golden/ex3-undef.c:11:9
In generate_value at test-data/golden/ex3-undef.c:11:9
In get_value at test-data/golden/ex3-undef.c:18:12
In main at test-data/golden/ex3-undef.c:25:5