Skip to main content


The following command checks all examples that we know to work. It completes in about 20s on my machine.

export RUST_LOG="caesar=trace"
cd pgcl/examples-heyvl
cargo run --release -- --raw unif_gen1.heyvl rabin1.heyvl rabin2.heyvl brp1.heyvl geo1.heyvl

You can run the benchmark set with evaluations by executing fish (fish shell is required).

One possible output of fish | column -ts "," is the following:

Name             Result  Total Time  VCgen Time  SAT Check Time
brp1.heyvl IND 1.54s 0.02s 1.2s
brp2.heyvl OOM 17.39s
brp3.heyvl OOM 17.29s
fail-geo1.heyvl REF 0.18s 0s 0.03s
geo1.heyvl IND 0.2s 0s 0.04s
linear01.heyvl IND 0.19s 0s 0.02s
rabin1.heyvl IND 0.5s 0s 0.03s
rabin2.heyvl IND 13.95s 0.23s 10.1s
unif_gen1.heyvl IND 6.97s 0.02s 6.61s
unif_gen2.heyvl TO 0.52s
unif_gen3.heyvl TO 0.48s
unif_gen4.heyvl OOM 17.54s