How to reduce smt instability?(And use SHAKE/co)

[Pat-Lafon]

Hello! I am building a deductive synthesizer with a similar logic to refinement types and some of my queries exhibit this smt instability(In my case, slight changes to the environment like running the query from an smtlib file on the command line versus constructing it via Z3 ocaml bindings can be the difference to whether or not z3 terminates). I'm trying to find ways to address this.

I saw the paper "Context Pruning for More Robust SMT-based Program Verification" which points to this repository but it seems like most of your ReadMe documentation is for the previous paper on Mariposa. Following that, I was able to confirm that the query I gave to expr_wizard was unstable. (Via something like: ./src/exper_wizard.py single -i data/projs/stlc/base.z3/stlc_no_xor.smt2 -e debug -s z3_4_12_2_osx --clear-existing)

But I'm more interested in trying to debug my queries and am hoping to use the less documented shake and other commands(which so far I'm having limited success). It seems like what I am looking for is in the query_wizard?

I tried python src/query_wizard.py build-core -i data/myqueries/bst_node_rev.smt2 -o bst_build_core.smt2 -s z3_4_12_2_osx and while I got a new smt2 file that has a smaller word count, it actually turned a smt file that z3 terminated in less than a second into one that does not terminate.

I then tried some of the other commands like inst-z3, create-shake, and wombo-combo but I was not able to find my way around these commands.

Since I am using z3 4.12, I had to add the -s flag to some of these to avoid the default 4.13. I'm not sure if other non-default z3 versions are intended to work but I have included my patch if it is useful.

After adding the additional solver options, I ran into errors around the underlying call to mariposa expecting some attributes that weren't found.
python src/query_wizard.py wombo-combo -i data/myqueries/stlc_no_xor.smt2 -o stlc_wombo_combo.smt2 -s z3_4_12_2_osx would generate src/smt2action/target/release/mariposa -a inst-z3 -i stlc_wombo_combo.smt2/0.smt2 --z3-trace-log-path gen//c83b69830d.z3-trace --max-trace-insts=3000 -o stlc_wombo_combo.smt2/0.temp.smt2 which panics with thread 'main' panicked at src/query_io.rs:627:9: expecting attributes

For create-shake, this seems like what I want but it takes in a log file and score which I'm less sure about and seems to just do some processing. Is this for handling the output of one of the other commands like quake?

I apologize for miss-understanding your tool and would appreciate any pointers in reducing the instability of my smt queries. I have included sample smt files if that helps.

0001-add-solver-options-to-more-commands.patch

bst_node_rev.smt2.txt

stlc_no_xor.smt2.txt

[yizhou7]

Sorry the usage of shake is not very well documented. One would need to add ids to a query first, for example:

./src/smt2action/target/release/mariposa -a add-ids -i data/samples/lib-Lang-LinearSequence.i.dfy.Impl__LinearSequence__i.__default.AllocAndMoveLseq.smt2 -o ids.smt2

Then output the shake distances:

./src/smt2action/target/release/mariposa -a shake -i ids.smt2 --shake-log-path shake.log

The log file should map assertion ids to their depths, where a depth of 18446744073709551615 means an unreachable assertion.

You can also set a depth for pruning:

./src/smt2action/target/release/mariposa -a shake -i ids.smt2 --shake-max-depth=4 -o shake.smt2

If you would like to build a core, some command like this should work

src/query_wizard.py build-core -i ids.smt2 -o core.smt2 --timeout 120 -s z3_4_12_2 --restarts 10