Randomly incorrect result using only Booleans

[onethreeseven]

I discovered this when a puzzle solver I'm building broke unexpectedly:

$ ./z3 --version
Z3 version 4.8.15 - 64 bit
$ ./z3 smt.random_seed=13 random_unsound_result.smt2 
sat
sat
sat
$ ./z3 smt.random_seed=14 random_unsound_result.smt2 
sat
sat
unsat

(All three results should be sat.) I get the incorrect result about 1% of the time. The problem uses only Bool, not, and, or, and pb_eq.

I apologize for the size of the test case; I'll try to reduce it if I find time but for now it's basically the problem I was working on.

Tested on 4.8.14 and current master (6a412f7).

[onethreeseven]

Is there a way to replicate the behavior of Python's SimpleSolver() from the command line tool? I'm having (slightly) more luck reducing my test case using the simple solver but I can't figure out how to save the result.

[onethreeseven]

I managed to get similar results by calling .check() right after instantiating the solver so it is incremental the whole way. As a result I have a slightly reduced case (use seeds 62 and 63) that only needs one round of incremental assertions to trigger the bug. I'm still struggling to make a truly minimal case, though.

[onethreeseven]

I am sad to report that I tried out this change and upon searching over random seeds the misbehavior actually seems to happen more often. Here's a new pair of seeds on my updated test case:

~/code/z3/build$ ./z3 smt.random_seed=15 ../../z3-tests/random_unsound_result_2.smt2 
sat
sat
sat
~/code/z3/build$ ./z3 smt.random_seed=16 ../../z3-tests/random_unsound_result_2.smt2 
sat
sat
unsat

[onethreeseven]

I've added the crude bash script I was using to search for misbehaving random seeds. Tomorrow if I can I will continue trying to find a truly minimal test case.

[onethreeseven]

Tested against both the canned SMT file and my original application, all looks 👍! Thanks.