Some regression tests print different counterexamples depending on solver version

[brianhuffman]

The expected output for regression tests issue066.icry and issue093.icry includes witnesses for :sat and/or counterexample values. With z3-4.8.12, the values printed do not match the expected ones in the .stdout files.

We should modify the regression tests so that we never rely on arbitrary choices about counterexamples made by external solvers: Any :sat query should be designed to have only one possible satisfying assignment, so that the test will be deterministic.

[LeventErkok]

This is a common problem with SBV, and I wish there was a good way to deal with it. Constraining too much to get a "deterministic" result can render the problem rather artificial.

For the SBV backend, one idea is to use the model-validator:

Prelude Data.SBV> isSatisfiableWith z3{validateModel=True} $ \x -> x .> (10 :: SInteger)
True

So, instead of getting a counter-model, we just make sure that the result is sat, and the validateModel=True parameter makes sure the model returned by the solver really does satisfy the result.

I suspect What4 backend can implement something similar as well.

One place where this doesn't work all that well is doctests, which is common in SBV. I'm not sure if Cryptol has many of those; but something to keep in mind.

[RyanGlScott]

I just hit this recently with Z3 4.8.14, so I'll record the diffs here for posterity's sake. For issue066, the diff is:

26c26
< g {x = 0xffffffff, y = 0x00000000} = False
---
> g {x = 0xfffff7ff, y = 0x00000800} = False
28c28
< {result = False, arg1 = {x = 0xffffffff, y = 0x00000000}}
---
> {result = False, arg1 = {x = 0xfffff7ff, y = 0x00000800}}
34c34
< h 0x00 0x00 = False
---
> h 0xfe 0x00 = False
36,37c36,37
< {result = False, arg1 = 0x00, arg2 = 0x00}
< 0x00
---
> {result = False, arg1 = 0xfe, arg2 = 0x00}
> 0xfe
40c40
< h 0x00 0x01 = True
---
> h 0x3e 0x40 = True
42c42
< {result = True, arg1 = 0x00, arg2 = 0x01}
---
> {result = True, arg1 = 0x3e, arg2 = 0x40}

And for issue093, the diff is:

33c33
< t2 0xfffffffe 0xffffffff = True
---
> t2 0x00000000 0x00000000 = True

[RyanGlScott]

Another approach, already employed in 3ea5e9e, is to simply use :set show-examples=false at the top of the .icry file and avoid printing it. This would avoid needing to overly constrain the queries, at the expense of making the test cases show less output. Then again:

• Bind :sat and :prove counter example in REPL #66 was originally about making sure that it gets bound to a record value, and :t it is sufficient to check that without needing to inspect the particular value of it.
• :prove with no argument should implicitly prove all properties #93 was originally about making sure that :prove with no arguments proves all properties in scope, and this can be checked without needing to show examples.