Incompleteness: the hard-coded `fp.spacer.global=true` z3 option makes any nested loop whose inner body has a merging conditional unverifiable — an 11-clause system that z3 solves in 0.5s without it runs >5min with it

[coord-e]

Summary

Config::default in src/chc/solver.rs:120-127 hard-codes the z3 command line as

name: "z3".to_owned(),
args: vec[
    "fp.spacer.global=true".to_owned(),
    "fp.validate=true".to_owned(),
],
timeout: Some(std::time::Duration::from_secs(30)),

fp.spacer.global=true turns on Spacer's global guidance (subsume/concretize/conjecture lemma generation). On the CHC systems Thrust emits for a nested loop whose inner body contains a conditional that merges back into the loop, that heuristic does not converge: z3 runs indefinitely on a system it otherwise answers in half a second. Since the pattern is while … { while … { if … { … } … } }, this is not an exotic corner — it is most real loop-processing code, and every such program is rejected with Timeout(30s) no matter how much timeout budget is given.

The system is a plain, tiny, linear-arithmetic one; this is not a case of the verification condition being hard.

Reproducer

// nested_if.rs
#[thrust::callable]
fn check() {
    let mut total = 0;
    let mut i = 0;
    while i < 3 {
        let mut j = 0;
        while j < 3 {
            if j == 1 {
                total += 1;
            }
            j += 1;
        }
        i += 1;
    }
    assert!(total == 3);
}

fn main() {}

$ cargo run -- -Adead_code -C debug-assertions=false nested_if.rs
error: verification error: Timeout(30s)

error: aborting due to 1 previous error

Raising the budget does not help (THRUST_SOLVER_TIMEOUT_SECS=240 → Timeout(240s)). Dropping the one option does:

$ THRUST_SOLVER_ARGS='fp.validate=true' cargo run -- -Adead_code -C debug-assertions=false nested_if.rs && echo safe
safe          # 0.7s wall clock

The system itself is trivial

Dumping it with THRUST_OUTPUT_DIR gives 11 clauses over 8 predicates (two of which, the loop heads, are non-nullary: arities 3 and 2), pure LIA apart from the Mut<Int> datatype constructors that total += 1 introduces. Handing that same file to z3 directly:

z3 invocation	result
z3 fp.spacer.global=true fp.validate=true out.smt2	no answer after 300s (killed)
z3 fp.spacer.global=true out.smt2	no answer after 60s (killed)
z3 fp.validate=true out.smt2	sat in 0.53s
z3 out.smt2	sat in 0.53s

So fp.validate is innocent; fp.spacer.global alone is what diverges.

Scope

Measured on 2bf022d with z3 5.0.0 (the version .github/actions/setup-z3 pins), 60s solver budget, -Adead_code -C debug-assertions=false:

program	default args	THRUST_SOLVER_ARGS='fp.validate=true'
nested loop, if in inner body (above)	Timeout(60s)	safe, 0.7s
same, with the weaker assert!(total <= 9)	Timeout(60s)	safe, 3.6s
nested loop, if/else in inner body	Timeout(60s)	safe, 0.8s
nested loop, continue in inner body	Timeout(60s)	safe, 0.8s
nested loop, continue + break in inner body	Timeout(60s)	safe, 0.6s
nested loop, two counters under if/else	Timeout(60s)	safe, 18.3s
nested loop, v.push(j) under an if	Timeout(60s)	safe, 1.9s
nested loop, if i <= j (provable both ways)	safe, 23.5s	safe, 2.1s
nested loop, no conditional in inner body	safe, 1.9s	safe, 0.8s
single loop with a conditional	safe, 0.3s	safe, 0.3s

The pattern is sharp: a single loop with a branch is fine, and a nested loop without a branch is fine; it is the combination — where the inner loop head needs a disjunctive invariant relating the accumulator to both loop counters — that global guidance never closes.

Why the option cannot simply be deleted

Removing fp.spacer.global=true from the default and running the suite gives 341 passed; 1 failed — tests/ui/pass/mut_recursive.rs (recursive fn sum(a: &mut i64, i: i64)) regresses to Timeout(60s). On its dumped system:

z3 invocation	result
z3 fp.spacer.global=true fp.validate=true out.smt2	sat in 0.25s
z3 fp.validate=true out.smt2	no answer after 300s (killed)

The two configurations are complementary, not ordered: recursion through a &mut prophecy wants global guidance, nested loops are destroyed by it. Baseline for reference: the suite is 342 passed with the option on.

Suggested fix

Solve with a portfolio rather than one hard-coded configuration: spawn z3 both with and without fp.spacer.global=true and take the first conclusive sat/unsat, reporting Timeout only when every configuration exhausts the budget. CommandConfig::run already spawns a child process with its own timeout, so this is mostly a matter of racing two of them in Config::check_sat and killing the loser (the SIGTERM cleanup added in #218 is already there). Both of the above cases then finish in under a second.

Failing that, at minimum the two configurations need to be reachable without THRUST_SOLVER_ARGS, which today replaces the whole argument list (CommandConfig::load_args) and so silently drops fp.validate as well — it is a workaround a user has to find by reading the source, not an interface.

Environment

• 2bf022d (Let a ghost term name generic- and Self-typed variables (#232))
• z3 5.0.0 x64-glibc-2.39, as pinned by .github/actions/setup-z3