Error when elaborating uncrowding resolution step

[NotBad4U]

Versions:

• carcara version: carcara 1.1.0 [git main 113f5a7] (current the last commit)
• cvc5 version: cvc5 1.2.1-dev.144.38fcc340e5 [git 38fcc340e5 on branch main]

Hi everyone!

When I try to elaborate some files from the SMT-lib bench like this one: QF_UF_sokoban.3.prop1_ab_br_max.smt2
I got this error: uncrowding.rs#L199 :"current clause is not a subset of target clause!".

I generated the proof with the command:

cvc5 --dag-thresh=2 --produce-proofs --dump-proofs --proof-format-mode=alethe --proof-granularity=dsl-rewrite --proof-alethe-res-pivots --proof-elim-subtypes --print-arith-lit-token QF_UF_sokoban.3.prop1_ab_br_max.smt2 >  QF_UF_sokoban.3.prop1_ab_br_max.alethe

This is my Carcara output:

cargo run -- elaborate --ignore-unknown-rules --expand-let-bindings QF_UF_sokoban.3.prop1_ab_br_max.alethe QF_UF_sokoban.3.prop1_ab_br_max.smt2
    Finished `dev` profile [unoptimized + debuginfo] target(s) in 0.07s
     Running `target/debug/carcara elaborate --ignore-unknown-rules --expand-let-bindings QF_UF_sokoban.3.prop1_ab_br_max.alethe QF_UF_sokoban.3.prop1_ab_br_max.smt2`
thread 'main' panicked at carcara/src/elaborator/uncrowding.rs:199:31:
current clause is not a subset of target clause!
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

I tried to run it with the --uncrowd-rotate but I got this error:

cargo run -- elaborate --uncrowd-rotate --ignore-unknown-rules --expand-let-bindings QF_UF_sokoban.3.prop1_ab_br_max.alethe QF_UF_sokoban.3.prop1_ab_br_max.smt2
    Finished `dev` profile [unoptimized + debuginfo] target(s) in 0.03s
     Running `target/debug/carcara elaborate --uncrowd-rotate --ignore-unknown-rules --expand-let-bindings QF_UF_sokoban.3.prop1_ab_br_max.alethe QF_UF_sokoban.3.prop1_ab_br_max.smt2`
thread 'main' panicked at carcara/src/elaborator/uncrowding.rs:326:69:
attempt to subtract with overflow
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

Note that I have no idea what this option it supposed to do...I was just looking at something that deals with uncrowd 😆 ...

A more recent version of CVC5 could fix my problem, or do we have a bug in the Carcara elaborator? 🤔
This error happens on many benchmark samples (when the proof starts to be long), which is quite blocking my progression.

[bpandreotti]

Thanks for the report! This is certainly a bug in Carcara. We generally only panic in situations that should never happen, so panics are always considered bugs. In the worst case, Carcara should at least return a nice error message. Still, in the case of resolution uncrowding, I expect a proof that checks without errors (which is the case), to be able to be uncrowded without errors. So the uncrowding algorithm is probably missing an edge case --- I will take a look.