ICE: failed to run fixpoint ... EOF while parsing a value

[enjhnsn2]

In response to Z3 hanging, Ranjit and Vivienne recomended I try using CVC5 to see if that just fixes the problem. However, after adding solver="cvc5" to Tock's flux.toml, Flux throws a very opaque ICE:

error: internal compiler error: crates/flux-infer/src/fixpoint_encoding.rs:436:35: failed to run fixpoint: Custom { kind: UnexpectedEof, error: Error("EOF while parsing a value", line: 1, column: 0) }

Any advice on debugging this error would be greatly appreciated.

This ICE can be reproduced by adding solver="cvc5" to flux.tomlintock/, entering tock/kernel, and running cargo flux.

[enjhnsn2]

LLM begone

[nilehmann]

1. You can FLUX_DUMP_CONSTRAINT=1 and run fixpoint directly on the *.smt2 file.
2. You can put #[flux_rs::opts(solver = "cvc5")] on top of a function to only check that function with cvc5.