Skip to content

Reloading proof crashes on with nix installation #1067

Open
Bug
Open
Reloading proof crashes on with nix installation#1067
Bug
Labels
bugSomething isn't working
@dkcumming

Description

@dkcumming
dkcumming
opened on Apr 16, 2026

When kmir is install via kup reloading a proof with --reload errors with:

INFO 2026-04-17 01:29:51,806 kmir.kompile - Writing Haskell definition file
INFO 2026-04-17 01:29:51,817 kmir.kompile - Copying other artefacts into HS output directory
Traceback (most recent call last):
  File "/nix/store/qbjyqg0pmksmiymx8yn1x4qzlqyzb767-kmir-0.4.206/bin/kmir", line 10, in <module>
    sys.exit(main())
  File "/nix/store/jpwzni5bqs4w2nkxgx4d94ylzp95mqpf-kmir-pyk-env/lib/python3.10/site-packages/kmir/__main__.py", line 757, in main
    kmir(sys.argv[1:])
  File "/nix/store/jpwzni5bqs4w2nkxgx4d94ylzp95mqpf-kmir-pyk-env/lib/python3.10/site-packages/kmir/__main__.py", line 306, in kmir
    _kmir_prove(opts)
  File "/nix/store/jpwzni5bqs4w2nkxgx4d94ylzp95mqpf-kmir-pyk-env/lib/python3.10/site-packages/kmir/__main__.py", line 85, in _kmir_prove
    proof = KMIR.prove_program(opts)
  File "/nix/store/jpwzni5bqs4w2nkxgx4d94ylzp95mqpf-kmir-pyk-env/lib/python3.10/site-packages/kmir/kmir.py", line 127, in prove_program
    return prove(opts)
  File "/nix/store/jpwzni5bqs4w2nkxgx4d94ylzp95mqpf-kmir-pyk-env/lib/python3.10/site-packages/kmir/_prove.py", line 45, in prove
    return _prove(opts, target_path, label)
  File "/nix/store/jpwzni5bqs4w2nkxgx4d94ylzp95mqpf-kmir-pyk-env/lib/python3.10/site-packages/kmir/_prove.py", line 89, in _prove
    kmir = KMIR.from_kompiled_kore(
  File "/nix/store/jpwzni5bqs4w2nkxgx4d94ylzp95mqpf-kmir-pyk-env/lib/python3.10/site-packages/kmir/kmir.py", line 70, in from_kompiled_kore
    kompiled_smir = kompile_smir(
  File "/nix/store/jpwzni5bqs4w2nkxgx4d94ylzp95mqpf-kmir-pyk-env/lib/python3.10/site-packages/kmir/kompile.py", line 339, in kompile_smir
    shutil.copy2(file_path, target_hs_path / file_path.name)
  File "/nix/store/hg8z7jqs9pwg114dh6s34iqrv5aswmrw-python3-3.10.14/lib/python3.10/shutil.py", line 434, in copy2
    copyfile(src, dst, follow_symlinks=follow_symlinks)
  File "/nix/store/hg8z7jqs9pwg114dh6s34iqrv5aswmrw-python3-3.10.14/lib/python3.10/shutil.py", line 256, in copyfile
    with open(dst, 'wb') as fdst:

A workaround is deleting the proof from the proof directory. Detailed logs below:

Details 
zncv@zncv-Prime-16-NP60SND ~$ kmir prove unchecked_add.rs --proof-dir kmir-proofs/ --start-symbol unchecked_add_u128_fail --verbose
INFO 2026-04-17 01:27:40,142 kmir._prove - Constructing initial proof: unchecked_add.unchecked_add_u128_fail
INFO 2026-04-17 01:27:40,142 pyk.utils - [PID=72859][exec] /nix/store/kds0fzp92l73gylwg8qivbjmzf0nafsa-stable-mir-json-0.2.0/bin/stable_mir_json -Zno-codegen /home/zncv/unchecked_add.rs
INFO 2026-04-17 01:27:40,156 pyk.utils - [PID=72859][stde] warning: the feature `unchecked_math` has been stable since 1.79.0 and no longer requires an attribute to enable
INFO 2026-04-17 01:27:40,156 pyk.utils - [PID=72859][stde]  --> /home/zncv/unchecked_add.rs:1:12
INFO 2026-04-17 01:27:40,156 pyk.utils - [PID=72859][stde]   |
INFO 2026-04-17 01:27:40,156 pyk.utils - [PID=72859][stde] 1 | #![feature(unchecked_math)]
INFO 2026-04-17 01:27:40,156 pyk.utils - [PID=72859][stde]   |            ^^^^^^^^^^^^^^
INFO 2026-04-17 01:27:40,156 pyk.utils - [PID=72859][stde]   |
INFO 2026-04-17 01:27:40,156 pyk.utils - [PID=72859][stde]   = note: `#[warn(stable_features)]` on by default
INFO 2026-04-17 01:27:40,156 pyk.utils - [PID=72859][stde] 
INFO 2026-04-17 01:27:40,167 pyk.utils - [PID=72859][stde] warning: 1 warning emitted
INFO 2026-04-17 01:27:40,167 pyk.utils - [PID=72859][stde] 
INFO 2026-04-17 01:27:40,169 pyk.utils - [PID=72859][done] status=0 time=0.027s
INFO 2026-04-17 01:27:40,170 kmir.cargo - Loaded: /home/zncv/unchecked_add.smir.json
INFO 2026-04-17 01:27:40,170 kmir.cargo - Deleted: /home/zncv/unchecked_add.smir.json
INFO 2026-04-17 01:27:40,171 kmir.kompile - Kompiling SMIR program: /home/zncv/kmir-proofs/unchecked_add.unchecked_add_u128_fail
INFO 2026-04-17 01:27:40,171 pyk.kdist._cache - Loading target cache
INFO 2026-04-17 01:27:40,172 pyk.kdist._cache - Loading plugin: mir-semantics
INFO 2026-04-17 01:27:40,172 pyk.kdist._cache - Importing module: kmir.kdist.plugin
INFO 2026-04-17 01:27:40,172 pyk.kdist._cache - Target cache loaded in 0.001s
INFO 2026-04-17 01:27:40,175 pyk.kast.outer - Loading JSON definition: /nix/store/v4aks8gzjd5ndk5hjpyg879rj5p8wmza-kmir-f5608f3fcfa2caea2a39ed54aca57c9b38fe05e8/mir-semantics/haskell/compiled.json
INFO 2026-04-17 01:27:40,219 pyk.kast.outer - Converting JSON definition to Kast: /nix/store/v4aks8gzjd5ndk5hjpyg879rj5p8wmza-kmir-f5608f3fcfa2caea2a39ed54aca57c9b38fe05e8/mir-semantics/haskell/compiled.json
INFO 2026-04-17 01:27:40,582 kmir.kompile - Generated 106 function equations to add to `definition.kore
INFO 2026-04-17 01:27:40,582 kmir.kompile - Creating directories /home/zncv/kmir-proofs/unchecked_add.unchecked_add_u128_fail/llvm-library/dt and /home/zncv/kmir-proofs/unchecked_add.unchecked_add_u128_fail/haskell
INFO 2026-04-17 01:27:40,582 kmir.kompile - Writing LLVM definition file
INFO 2026-04-17 01:27:40,592 kmir.kompile - Running llvm-kompile-matching
INFO 2026-04-17 01:27:43,382 kmir.kompile - Running llvm-kompile
INFO 2026-04-17 01:28:19,586 kmir.kompile - Writing Haskell definition file
INFO 2026-04-17 01:28:19,595 kmir.kompile - Copying other artefacts into HS output directory
INFO 2026-04-17 01:28:19,605 pyk.kast.outer - Loading JSON definition: /home/zncv/kmir-proofs/unchecked_add.unchecked_add_u128_fail/haskell/compiled.json
INFO 2026-04-17 01:28:19,689 pyk.kast.outer - Converting JSON definition to Kast: /home/zncv/kmir-proofs/unchecked_add.unchecked_add_u128_fail/haskell/compiled.json
INFO 2026-04-17 01:28:19,884 pyk.utils - Making directory: /home/zncv/kmir-proofs/unchecked_add.unchecked_add_u128_fail/kcfg
INFO 2026-04-17 01:28:19,884 pyk.utils - Making directory: /home/zncv/kmir-proofs/unchecked_add.unchecked_add_u128_fail/kcfg/nodes
INFO 2026-04-17 01:28:19,885 pyk.kore.rpc - Starting KoreServer: kore-rpc-booster /home/zncv/kmir-proofs/unchecked_add.unchecked_add_u128_fail/haskell/definition.kore --module KMIR --server-port 0 --llvm-backend-library /home/zncv/kmir-proofs/unchecked_add.unchecked_add_u128_fail/llvm-library/interpreter.so --simplify-each 30
INFO 2026-04-17 01:28:19,893 pyk.kore.rpc - [PID=73083][stde] [proxy] Loading definition from /home/zncv/kmir-proofs/unchecked_add.unchecked_add_u128_fail/haskell/definition.kore, main module "KMIR"
INFO 2026-04-17 01:28:20,898 pyk.kore.rpc - [PID=73083][stde] [kore][info] Reading the input file TimeSpec {sec = 0, nsec = 10550019}
INFO 2026-04-17 01:28:20,898 pyk.kore.rpc - [PID=73083][stde] [kore][info] Parsing the file TimeSpec {sec = 0, nsec = 202}
INFO 2026-04-17 01:28:21,918 pyk.kore.rpc - [PID=73083][stde] [kore][info] Verifying the definition TimeSpec {sec = 0, nsec = 260}
INFO 2026-04-17 01:28:21,918 pyk.kore.rpc - [PID=73083][stde] [kore][info] Executing TimeSpec {sec = 0, nsec = 499672809}
INFO 2026-04-17 01:28:21,918 pyk.kore.rpc - [PID=73083][stde] [kore][info] Reading the input file TimeSpec {sec = 0, nsec = 9914168}
INFO 2026-04-17 01:28:21,918 pyk.kore.rpc - [PID=73083][stde] [kore][info] Parsing the file TimeSpec {sec = 0, nsec = 227}
INFO 2026-04-17 01:28:22,387 pyk.kore.rpc - KoreServer started: 0.0.0.0:39405, pid=73083
INFO 2026-04-17 01:28:22,387 pyk.kore.rpc - Connecting to host: localhost:39405
INFO 2026-04-17 01:28:22,387 pyk.kore.rpc - Connected to host: localhost:39405
INFO 2026-04-17 01:28:22,387 pyk.proof.proof - Initializing proof: unchecked_add.unchecked_add_u128_fail
INFO 2026-04-17 01:28:22,388 pyk.kore.rpc - Sending request to localhost:39405: 129634611086672-001 - add-module
INFO 2026-04-17 01:28:22,888 pyk.kore.rpc - Received response from localhost:39405: 129634611086672-001 - add-module
INFO 2026-04-17 01:28:22,889 pyk.proof.proof - Found 1 next steps for proof: unchecked_add.unchecked_add_u128_fail
INFO 2026-04-17 01:28:22,896 pyk.kore.rpc - Sending request to localhost:39405: 129634611086672-002 - execute
INFO 2026-04-17 01:28:22,938 pyk.kore.rpc - [PID=73083][stde] [kore][info] Verifying the definition TimeSpec {sec = 0, nsec = 273}
INFO 2026-04-17 01:28:22,938 pyk.kore.rpc - [PID=73083][stde] [proxy] Starting RPC server
INFO 2026-04-17 01:28:22,938 pyk.kore.rpc - [PID=73083][stde] [proxy] Processing request 129634611086672-001
INFO 2026-04-17 01:28:22,938 pyk.kore.rpc - [PID=73083][stde] [proxy] Processing request 129634611086672-002
INFO 2026-04-17 01:28:25,379 pyk.kore.rpc - Received response from localhost:39405: 129634611086672-002 - execute
INFO 2026-04-17 01:28:25,397 pyk.kcfg.kcfg - Extending KCFG with: basic block at depth 56: 1 --> 3
// -snip-
APRProof: unchecked_add.unchecked_add_u128_fail
    status: ProofStatus.FAILED
    admitted: False
    nodes: 11
    pending: 0
    failing: 1
    vacuous: 0
    stuck: 1
    terminal: 3
    refuted: 0
    bounded: 0
    execution time: 0s
Subproofs: 0
zncv@zncv-Prime-16-NP60SND ~$ kup list
┌──────────────────────┬─────────────────────────────────────────────────────┬──────────────┐
│ Package name (alias) │ Installed version                                   │ Status       │
├──────────────────────┼─────────────────────────────────────────────────────┼──────────────┤
│ kup                  │ 9cff6f6596ca1bd7accb53c4178f71d146a69997            │ 🟢 installed │
│ kmir                 │ f5608f3fcfa2caea2a39ed54aca57c9b38fe05e8 (v0.4.206) │ 🟢 installed │
│ k                    │                                                     │ 🔵 available │
│ kavm                 │                                                     │ 🔵 available │
│ kevm                 │                                                     │ 🔵 available │
│ kplutus              │                                                     │ 🔵 available │
│ kontrol              │                                                     │ 🔵 available │
│ kmxwasm              │                                                     │ 🔵 available │
│ komet                │                                                     │ 🔵 available │
│ skribe               │                                                     │ 🔵 available │
└──────────────────────┴─────────────────────────────────────────────────────┴──────────────┘
zncv@zncv-Prime-16-NP60SND ~$ kmir prove unchecked_add.rs --proof-dir kmir-proofs/ --start-symbol unchecked_add_u128_fail --verbose --reload
INFO 2026-04-17 01:29:12,632 kmir._prove - Constructing initial proof: unchecked_add.unchecked_add_u128_fail
INFO 2026-04-17 01:29:12,633 pyk.utils - [PID=73357][exec] /nix/store/kds0fzp92l73gylwg8qivbjmzf0nafsa-stable-mir-json-0.2.0/bin/stable_mir_json -Zno-codegen /home/zncv/unchecked_add.rs
INFO 2026-04-17 01:29:12,643 pyk.utils - [PID=73357][stde] warning: the feature `unchecked_math` has been stable since 1.79.0 and no longer requires an attribute to enable
INFO 2026-04-17 01:29:12,643 pyk.utils - [PID=73357][stde]  --> /home/zncv/unchecked_add.rs:1:12
INFO 2026-04-17 01:29:12,643 pyk.utils - [PID=73357][stde]   |
INFO 2026-04-17 01:29:12,643 pyk.utils - [PID=73357][stde] 1 | #![feature(unchecked_math)]
INFO 2026-04-17 01:29:12,643 pyk.utils - [PID=73357][stde]   |            ^^^^^^^^^^^^^^
INFO 2026-04-17 01:29:12,643 pyk.utils - [PID=73357][stde]   |
INFO 2026-04-17 01:29:12,643 pyk.utils - [PID=73357][stde]   = note: `#[warn(stable_features)]` on by default
INFO 2026-04-17 01:29:12,643 pyk.utils - [PID=73357][stde] 
INFO 2026-04-17 01:29:12,650 pyk.utils - [PID=73357][stde] warning: 1 warning emitted
INFO 2026-04-17 01:29:12,650 pyk.utils - [PID=73357][stde] 
INFO 2026-04-17 01:29:12,653 pyk.utils - [PID=73357][done] status=0 time=0.020s
INFO 2026-04-17 01:29:12,654 kmir.cargo - Loaded: /home/zncv/unchecked_add.smir.json
INFO 2026-04-17 01:29:12,654 kmir.cargo - Deleted: /home/zncv/unchecked_add.smir.json
INFO 2026-04-17 01:29:12,655 kmir.kompile - Kompiling SMIR program: /home/zncv/kmir-proofs/unchecked_add.unchecked_add_u128_fail
INFO 2026-04-17 01:29:12,655 pyk.kdist._cache - Loading target cache
INFO 2026-04-17 01:29:12,656 pyk.kdist._cache - Loading plugin: mir-semantics
INFO 2026-04-17 01:29:12,657 pyk.kdist._cache - Importing module: kmir.kdist.plugin
INFO 2026-04-17 01:29:12,657 pyk.kdist._cache - Target cache loaded in 0.001s
INFO 2026-04-17 01:29:12,660 pyk.kast.outer - Loading JSON definition: /nix/store/v4aks8gzjd5ndk5hjpyg879rj5p8wmza-kmir-f5608f3fcfa2caea2a39ed54aca57c9b38fe05e8/mir-semantics/haskell/compiled.json
INFO 2026-04-17 01:29:12,705 pyk.kast.outer - Converting JSON definition to Kast: /nix/store/v4aks8gzjd5ndk5hjpyg879rj5p8wmza-kmir-f5608f3fcfa2caea2a39ed54aca57c9b38fe05e8/mir-semantics/haskell/compiled.json
INFO 2026-04-17 01:29:13,097 kmir.kompile - Generated 106 function equations to add to `definition.kore
INFO 2026-04-17 01:29:13,097 kmir.kompile - Creating directories /home/zncv/kmir-proofs/unchecked_add.unchecked_add_u128_fail/llvm-library/dt and /home/zncv/kmir-proofs/unchecked_add.unchecked_add_u128_fail/haskell
INFO 2026-04-17 01:29:13,097 kmir.kompile - Writing LLVM definition file
INFO 2026-04-17 01:29:13,110 kmir.kompile - Running llvm-kompile-matching
INFO 2026-04-17 01:29:15,779 kmir.kompile - Running llvm-kompile
INFO 2026-04-17 01:29:51,806 kmir.kompile - Writing Haskell definition file
INFO 2026-04-17 01:29:51,817 kmir.kompile - Copying other artefacts into HS output directory
Traceback (most recent call last):
  File "/nix/store/qbjyqg0pmksmiymx8yn1x4qzlqyzb767-kmir-0.4.206/bin/kmir", line 10, in <module>
    sys.exit(main())
  File "/nix/store/jpwzni5bqs4w2nkxgx4d94ylzp95mqpf-kmir-pyk-env/lib/python3.10/site-packages/kmir/__main__.py", line 757, in main
    kmir(sys.argv[1:])
  File "/nix/store/jpwzni5bqs4w2nkxgx4d94ylzp95mqpf-kmir-pyk-env/lib/python3.10/site-packages/kmir/__main__.py", line 306, in kmir
    _kmir_prove(opts)
  File "/nix/store/jpwzni5bqs4w2nkxgx4d94ylzp95mqpf-kmir-pyk-env/lib/python3.10/site-packages/kmir/__main__.py", line 85, in _kmir_prove
    proof = KMIR.prove_program(opts)
  File "/nix/store/jpwzni5bqs4w2nkxgx4d94ylzp95mqpf-kmir-pyk-env/lib/python3.10/site-packages/kmir/kmir.py", line 127, in prove_program
    return prove(opts)
  File "/nix/store/jpwzni5bqs4w2nkxgx4d94ylzp95mqpf-kmir-pyk-env/lib/python3.10/site-packages/kmir/_prove.py", line 45, in prove
    return _prove(opts, target_path, label)
  File "/nix/store/jpwzni5bqs4w2nkxgx4d94ylzp95mqpf-kmir-pyk-env/lib/python3.10/site-packages/kmir/_prove.py", line 89, in _prove
    kmir = KMIR.from_kompiled_kore(
  File "/nix/store/jpwzni5bqs4w2nkxgx4d94ylzp95mqpf-kmir-pyk-env/lib/python3.10/site-packages/kmir/kmir.py", line 70, in from_kompiled_kore
    kompiled_smir = kompile_smir(
  File "/nix/store/jpwzni5bqs4w2nkxgx4d94ylzp95mqpf-kmir-pyk-env/lib/python3.10/site-packages/kmir/kompile.py", line 339, in kompile_smir
    shutil.copy2(file_path, target_hs_path / file_path.name)
  File "/nix/store/hg8z7jqs9pwg114dh6s34iqrv5aswmrw-python3-3.10.14/lib/python3.10/shutil.py", line 434, in copy2
    copyfile(src, dst, follow_symlinks=follow_symlinks)
  File "/nix/store/hg8z7jqs9pwg114dh6s34iqrv5aswmrw-python3-3.10.14/lib/python3.10/shutil.py", line 256, in copyfile
    with open(dst, 'wb') as fdst:
zncv@zncv-Prime-16-NP60SND ~$ echo $?
1
zncv@zncv-Prime-16-NP60SND ~$ rm -rf kmir-proofs/
zncv@zncv-Prime-16-NP60SND ~$ kmir prove unchecked_add.rs --proof-dir kmir-proofs/ --start-symbol unchecked_add_u128_fail --verbose --reload
INFO 2026-04-17 01:34:13,925 kmir._prove - Constructing initial proof: unchecked_add.unchecked_add_u128_fail
INFO 2026-04-17 01:34:13,925 pyk.utils - [PID=73654][exec] /nix/store/kds0fzp92l73gylwg8qivbjmzf0nafsa-stable-mir-json-0.2.0/bin/stable_mir_json -Zno-codegen /home/zncv/unchecked_add.rs
INFO 2026-04-17 01:34:13,936 pyk.utils - [PID=73654][stde] warning: the feature `unchecked_math` has been stable since 1.79.0 and no longer requires an attribute to enable
INFO 2026-04-17 01:34:13,936 pyk.utils - [PID=73654][stde]  --> /home/zncv/unchecked_add.rs:1:12
INFO 2026-04-17 01:34:13,936 pyk.utils - [PID=73654][stde]   |
INFO 2026-04-17 01:34:13,936 pyk.utils - [PID=73654][stde] 1 | #![feature(unchecked_math)]
INFO 2026-04-17 01:34:13,936 pyk.utils - [PID=73654][stde]   |            ^^^^^^^^^^^^^^
INFO 2026-04-17 01:34:13,936 pyk.utils - [PID=73654][stde]   |
INFO 2026-04-17 01:34:13,936 pyk.utils - [PID=73654][stde]   = note: `#[warn(stable_features)]` on by default
INFO 2026-04-17 01:34:13,936 pyk.utils - [PID=73654][stde] 
INFO 2026-04-17 01:34:13,944 pyk.utils - [PID=73654][stde] warning: 1 warning emitted
INFO 2026-04-17 01:34:13,944 pyk.utils - [PID=73654][stde] 
INFO 2026-04-17 01:34:13,947 pyk.utils - [PID=73654][done] status=0 time=0.021s
INFO 2026-04-17 01:34:13,947 kmir.cargo - Loaded: /home/zncv/unchecked_add.smir.json
INFO 2026-04-17 01:34:13,947 kmir.cargo - Deleted: /home/zncv/unchecked_add.smir.json
INFO 2026-04-17 01:34:13,949 kmir.kompile - Kompiling SMIR program: /home/zncv/kmir-proofs/unchecked_add.unchecked_add_u128_fail
INFO 2026-04-17 01:34:13,949 pyk.kdist._cache - Loading target cache
INFO 2026-04-17 01:34:13,950 pyk.kdist._cache - Loading plugin: mir-semantics
INFO 2026-04-17 01:34:13,950 pyk.kdist._cache - Importing module: kmir.kdist.plugin
INFO 2026-04-17 01:34:13,950 pyk.kdist._cache - Target cache loaded in 0.001s
INFO 2026-04-17 01:34:13,953 pyk.kast.outer - Loading JSON definition: /nix/store/v4aks8gzjd5ndk5hjpyg879rj5p8wmza-kmir-f5608f3fcfa2caea2a39ed54aca57c9b38fe05e8/mir-semantics/haskell/compiled.json
INFO 2026-04-17 01:34:13,999 pyk.kast.outer - Converting JSON definition to Kast: /nix/store/v4aks8gzjd5ndk5hjpyg879rj5p8wmza-kmir-f5608f3fcfa2caea2a39ed54aca57c9b38fe05e8/mir-semantics/haskell/compiled.json
INFO 2026-04-17 01:34:14,363 kmir.kompile - Generated 106 function equations to add to `definition.kore
INFO 2026-04-17 01:34:14,363 kmir.kompile - Creating directories /home/zncv/kmir-proofs/unchecked_add.unchecked_add_u128_fail/llvm-library/dt and /home/zncv/kmir-proofs/unchecked_add.unchecked_add_u128_fail/haskell
INFO 2026-04-17 01:34:14,363 kmir.kompile - Writing LLVM definition file
INFO 2026-04-17 01:34:14,373 kmir.kompile - Running llvm-kompile-matching
INFO 2026-04-17 01:34:17,150 kmir.kompile - Running llvm-kompile
INFO 2026-04-17 01:34:53,377 kmir.kompile - Writing Haskell definition file
INFO 2026-04-17 01:34:53,387 kmir.kompile - Copying other artefacts into HS output directory
INFO 2026-04-17 01:34:53,397 pyk.kast.outer - Loading JSON definition: /home/zncv/kmir-proofs/unchecked_add.unchecked_add_u128_fail/haskell/compiled.json
INFO 2026-04-17 01:34:53,482 pyk.kast.outer - Converting JSON definition to Kast: /home/zncv/kmir-proofs/unchecked_add.unchecked_add_u128_fail/haskell/compiled.json
INFO 2026-04-17 01:34:53,679 pyk.utils - Making directory: /home/zncv/kmir-proofs/unchecked_add.unchecked_add_u128_fail/kcfg
INFO 2026-04-17 01:34:53,679 pyk.utils - Making directory: /home/zncv/kmir-proofs/unchecked_add.unchecked_add_u128_fail/kcfg/nodes
INFO 2026-04-17 01:34:53,680 pyk.kore.rpc - Starting KoreServer: kore-rpc-booster /home/zncv/kmir-proofs/unchecked_add.unchecked_add_u128_fail/haskell/definition.kore --module KMIR --server-port 0 --llvm-backend-library /home/zncv/kmir-proofs/unchecked_add.unchecked_add_u128_fail/llvm-library/interpreter.so --simplify-each 30
INFO 2026-04-17 01:34:53,687 pyk.kore.rpc - [PID=73878][stde] [proxy] Loading definition from /home/zncv/kmir-proofs/unchecked_add.unchecked_add_u128_fail/haskell/definition.kore, main module "KMIR"
INFO 2026-04-17 01:34:54,692 pyk.kore.rpc - [PID=73878][stde] [kore][info] Reading the input file TimeSpec {sec = 0, nsec = 10113731}
INFO 2026-04-17 01:34:54,693 pyk.kore.rpc - [PID=73878][stde] [kore][info] Parsing the file TimeSpec {sec = 0, nsec = 252}
INFO 2026-04-17 01:34:55,713 pyk.kore.rpc - [PID=73878][stde] [kore][info] Verifying the definition TimeSpec {sec = 0, nsec = 245}
INFO 2026-04-17 01:34:55,713 pyk.kore.rpc - [PID=73878][stde] [kore][info] Executing TimeSpec {sec = 0, nsec = 495165574}
INFO 2026-04-17 01:34:55,713 pyk.kore.rpc - [PID=73878][stde] [kore][info] Reading the input file TimeSpec {sec = 0, nsec = 10427125}
INFO 2026-04-17 01:34:55,713 pyk.kore.rpc - [PID=73878][stde] [kore][info] Parsing the file TimeSpec {sec = 0, nsec = 274}
INFO 2026-04-17 01:34:56,205 pyk.kore.rpc - KoreServer started: 0.0.0.0:41833, pid=73878
INFO 2026-04-17 01:34:56,205 pyk.kore.rpc - Connecting to host: localhost:41833
INFO 2026-04-17 01:34:56,205 pyk.kore.rpc - Connected to host: localhost:41833
INFO 2026-04-17 01:34:56,205 pyk.proof.proof - Initializing proof: unchecked_add.unchecked_add_u128_fail
INFO 2026-04-17 01:34:56,205 pyk.kore.rpc - Sending request to localhost:41833: 125139192939760-001 - add-module
INFO 2026-04-17 01:34:56,714 pyk.kore.rpc - [PID=73878][stde] [kore][info] Verifying the definition TimeSpec {sec = 0, nsec = 269}
INFO 2026-04-17 01:34:56,714 pyk.kore.rpc - [PID=73878][stde] [proxy] Starting RPC server
INFO 2026-04-17 01:34:56,714 pyk.kore.rpc - [PID=73878][stde] [proxy] Processing request 125139192939760-001
INFO 2026-04-17 01:34:56,714 pyk.kore.rpc - Received response from localhost:41833: 125139192939760-001 - add-module
INFO 2026-04-17 01:34:56,715 pyk.proof.proof - Found 1 next steps for proof: unchecked_add.unchecked_add_u128_fail
INFO 2026-04-17 01:34:56,722 pyk.kore.rpc - Sending request to localhost:41833: 125139192939760-002 - execute
INFO 2026-04-17 01:34:57,715 pyk.kore.rpc - [PID=73878][stde] [proxy] Processing request 125139192939760-002
INFO 2026-04-17 01:34:59,230 pyk.kore.rpc - Received response from localhost:41833: 125139192939760-002 - execute
INFO 2026-04-17 01:34:59,249 pyk.kcfg.kcfg - Extending KCFG with: basic block at depth 56: 1 --> 3
//-snip-
APRProof: unchecked_add.unchecked_add_u128_fail
    status: ProofStatus.FAILED
    admitted: False
    nodes: 11
    pending: 0
    failing: 1
    vacuous: 0
    stuck: 1
    terminal: 3
    refuted: 0
    bounded: 0
    execution time: 0s
Subproofs: 0

Metadata

Metadata

Assignees

No one assigned

    Labels

    bugSomething isn't working

    Type

    Bug

    Fields

    No fields configured for Bug.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions