Bug - Incorrect Optimum Result

[PatrickTrentin88]

commit: 185b01d
issue: z3 finds 49 as optimal result of opt.smt2, instead of 38
files: witnesses.zip
notes: The formula sat.smt2 forces the cost function to be equal 38, and the formula unsat.smt2 forces the cost function to be better than 38. The solver says that the first formula is satisfiable and the second formula is unsatisfiable.

[NikolajBjorner]

There were fixes to PB + SAT integration after the commit mentioned above. With current master Z3 returns 38.

[PatrickTrentin88]

I see, thanks.

[PatrickTrentin88]

commit: 9fa9aa0
issue: z3 finds 91 as optimum result of pc_32-4-8-2.new-gen_z3.smt2, instead of 92
files: pc_32-4-8-2.new-gen_z3.zip
notes: z3 confirms that the solution objective = 92 is satisfiable if such a constraint is added to the formula

[PatrickTrentin88]

@NikolajBjorner news?

[NikolajBjorner]

the example is not small and there have been other bugs to deal with

[PatrickTrentin88]

I'd like to apologize to you @NikolajBjorner for being disrespectful. Since I re-opened the previous issue instead of filing a new bug, I was unsure whether it had been noticed or not. No pressure at all.

[NikolajBjorner]

Not at all, bug reports are always extremely appreciated whether in same or new issue.
I have been on the road for a while and the issues are piling up. There are a couple of tough nuts regarding sequences and "nth" that are blocking context switch to other fronts.

[NikolajBjorner]

Is this latest version of Z3? Some observations:

• my first three tests with different random seeds use about 5min to solve the problem, the results are 92. The commit hash suggests the bug should be in current master, so perhaps fluctuating on random seeds.
• setting smt.arith.solver=6 makes it very slow. @levnach - you can extract a pure smt problem by removing the (maximize..) line from the pc_32-4-8-2.new-gen_z3 file to make repros simpler.
• set opt.elim_01=false makes the solving time drastically faster (and likely bypasses likely bug).

[PatrickTrentin88]

I used commit 9fa9aa0, which at the time I submitted the formula was the latest one. I did not manually set the random seed. The output i get is attached (out.txt). If there is a way for me to gather info on the random seed used and report it to you, please let me know.

I just confirmed the same problem with commit 2e6908b.

Indeed opt.elim_01=false yields the correct answer in shorter time.

[NikolajBjorner]

random seed is something we set from the command-line (or API). For this example, we can set smt.random_seed=1 or smt.random_seed=23 etc. It makes the solver explore different search ordering.

[levnach]

It reproduces both on Windows and Ubuntu in the last release of Z3. To reproduce the behavior just run "z3 pc_32-4-8-2.new-gen_z3.smt2" without any additional parameters and see that objective is 91.
I ran the debug version on the same file and got an assertion
ASSERTION VIOLATION
File: ../../src/smt/theory_pb.cpp
Line: 1864
validate_lemma()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[NikolajBjorner]

I was never able to get 91, however, the assert that Lev pointed to exposes a bug. A fix for this has been pushed.

[PatrickTrentin88]

Thanks!