Updating Z3 model_compress parameter.

[michael-emmi]

• Z3 4.8.7 consolidates model.compact and model_compress.

[michael-emmi]

@bkragl any ideas what should be done when test output varies from system to system? I’m getting different test failures on my own machine…

[zvonimir]

Looks good to me.

[bkragl]

On my system (Ubuntu / .NET Core) with Z3 4.8.4 I see the same four tests failing as in Travis:

test15/CaptureState.bpl
test15/IntInModel.bpl
test15/ModelTest.bpl
test15/NullInModel.bpl

All of them look benign. Just some small difference in the model output.

With Z3 4.8.7 I see the following tests fail:

aitest9/TestIntervals.bpl
extractloops/t3.bpl
livevars/bla1.bpl
livevars/stack_overflow.bpl
test15/CaptureState.bpl
test15/ModelTest.bpl
test2/Rlimitouts0.bpl
test7/MultipleErrors.bpl

@michael-emmi: Could this be the difference that you see? In any case, also there the failures are due to slightly different models/error traces (except test2/Rlimitouts0.bpl which tests different resource limits). I would say we could adapt the expected output for these tests and switch the testing in Travis to Z3 4.8.7.

In general I don't have a good strategy to make testing with different configurations (in particular different Z3 versions) stable.

@michael-emmi: In case you did not know, there is #73 where we started to discuss a cleanup of the Z3 options that Boogie sets by default. There is a branch z3-option-cleanup where I removed all but some minimal set of necessary options for testing (I'll rebase it onto the latest master to get the current .NET Core build).

[michael-emmi]

@bkragl I wasn’t aware of #73 but glad I am now — thanks!

Could this be the difference that you see?

Yes, those are precisely the differences I see.

So should this PR fix the expected test output so that they all pass on Travis with Z3 4.8.7?

[bkragl]

So should this PR fix the expected test output so that they all pass on Travis with Z3 4.8.7?

I think so. We could also fix the tests for Z3 4.8.4, but to me upgrading right away makes more sense.