Incremental formula with two unsat

[hernanponcedeleon]

./src/proj_wizard.py create fails if I have the attached formula in my project ticketlock-opt.ll.zip

> ./src/proj_wizard.py create -i data/dartagnan/ --new-project-name dartagnan
[INFO] output directory is set to data/projs/dartagnan/base.z3 
[INFO] generated 1 targets in build.ninja 
[1/1] src/smt2action/target/release/mariposa -i dat.../ticketlock-opt.ll.smt2 -a split --convert-comments
FAILED: data/projs/dartagnan/base.z3/ticketlock-opt.ll.smt2 
src/smt2action/target/release/mariposa -i data/dartagnan/ticketlock-opt.ll.smt2 -o data/projs/dartagnan/base.z3/ticketlock-opt.ll.smt2 -a split --convert-comments
thread 'main' panicked at src/query_io.rs:285:5:
assertion failed: !check_sat_depth_zero || max_depth == 0
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
ninja: build stopped: cannot make progress due to previous errors.
[INFO] generated 1 files in data/projs/dartagnan/base.z3 

There are several calls to check-sat. The first few ones are sat, while the last two are unsat. If I remove the latest check-sat, then ./src/proj_wizard.py create works correctly.

Is it expected that the formula has a single unsat?

[yizhou7]

I think there are two issues with Mariposa that you have stumbled upon.

Pre-processing

Mariposa's pre-processing makes an implicit assumption about how check-sat are nested.
Mariposa usually deals with queries with Dafny/F*/Verus, where a push-pop scope should only have a single "actual" check-sat, potentially followed by a few debugging check-sats. Mariposa removes the debugging check-sats and only keeps the first one in each scope.

SAT restult

For Mariposa's use case so far (Dafny/F*/Verus), SAT is an unexpected result. These queries always get an unknown upon failure, since undecidable theories are involved. I have not tested it extensively, but Mariposa will likely run into weird issues when the query is supposed to return SAT.

[hernanponcedeleon]

Let me give you some background or what I am trying to do, and hopefully you can help me decide if mariposa could help me.

My encoding represents all executions of a program: SAT means some execution has a bug, UNSAT the program is correct. I am fine with just focusing on safe programs if that means mariposa could help me.

The encoding is generated in an iterative way (in a CEGAR fashion). I start with a large encoding B1 and one extra initial small constraint B2 which (if the program is safe), I will eventually need to remove, thus the push. Then, each iteration i adds a small constrain Ci which is computed by an external procedure (the CEGAR refiner) if the current B & C1 & ... & Ci-1 is SAT. Thus, the encoding looks like this

B1
(push 1)
B2
(check-sat) // SAT
C1
(check-sat) // SAT
...
Cn
(check-sat) // UNSAT
(pop 1)
(check-sat) // UNSAT

Hopefully B2 does not contribute directly to my problem, so I am fine with simplifying the scenario to this

B1
(check-sat) // SAT
C1
(check-sat) // SAT
...
Cn
(check-sat) // UNSAT

My problem is that for some iterations the SMT is really fast, and for other it is really slow. I am trying to understand why there is so much different between solving B & C1 & ... & Ci-1 and B & C1 & ... & Ci considering that the difference is the encoding is "small". To give you some rough numbers, B can take half of the size of the whole encoding and I can have a few thousand iterations, meaning that each Ci contributed to 0.05 of the formula size.

If I understood you correctly, removing the intermediate (check-sat) would result in this, which mariposa should be able to handle

B1
C1
...
Cn
(check-sat) // UNSAT

What I wonder if the cases where I see slow iterations (this does not happen for all programs I analyze) corresponds to cases where mariposa would say the encoding is instable and if I can somehow use this to improve my encoding.

[parno]

What kinds of theories do your formulas use?

[hernanponcedeleon]

Bit vectors