search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.3k stars 1.48k forks source link

Breakage around optimization routines #1644

Closed LeventErkok closed 6 years ago

LeventErkok commented 6 years ago

@NikolajBjorner

I'm seeing some test failures with a very fresh Z3 build (https://travis-ci.org/LeventErkok/sbv/jobs/382869021#L3283)

Failures seem to be happening around optimization calls, but I haven't investigated in full yet.

Since you seem to be in the middle of a bunch of changes, I wanted to check if you'd rather I wait till the code-base stabilizes, or would rather hear about these right away. Please advise.

NikolajBjorner commented 6 years ago

It is good to get them sooner instead of later. Users who need stability should use 4.7.1 for some weeks. Users who have bandwidth to send bug reports should alert me.

This is a huge breaking change that I have been holding on to for many months, but now is the time to get this into the build. It includes updates in the SAT solver and pseudo-Boolean theory solver that could affect your test cases.

I am currently fixing build breaks for VS 2012, which few will care about other than our build machines.

NikolajBjorner commented 6 years ago

We have regression tests with every build. For your own regression tests, perhaps could you use the serializers to SMT-LIB and a corresponding "gold" output would let us run similar regressions on every CI build.

LeventErkok commented 6 years ago

Great! I'll report as I see issues.