Result changes from sat to unsat after duplication and-subexpression

[AnzhelaSukhanova]

Hello,

I have found a clause where a result changes from sat to unsat after duplication and-subexpression (line 50 of attached files). I have checked both examples with Eldarica and it has returned sat.

sat.smt2.txt
bug.smt2.txt

[NikolajBjorner]

@agurfinkel - https://github.com/AnzhelaSukhanova/fuzzing_of_spacer

[agurfinkel]

@AnzhelaSukhanova is it possible to minimize this example somewhat?

[NikolajBjorner]

More information is in the commit message:

It is not unlike other fuzz bugs: it exercises some behavior that applications are unlikely to expose. In this case, a rule body expanded into a conjunction with more than 1M formulas (with a lot of repetition). The original rule representation assumed silently that the number of constraints in a body would fit within 20 bits, but reality allowed bodies with as many as 2^{32} - 1 constraints.
So "minimizing" the bug as @agurfinkel asks for seems not to make too much sense.

Just running the samples in debug mode points to the root cause.

Since fuzz bugs are not from applications and fuzz tools have the potential for creating a large number of issues, I find it reasonable to push some basic pro-active asks on filers:

• reproduce bug in debug builds to assess whether a debug assert triggers.
• minimize or keep it simpler when possible (in this case it does not apply)
• perform basic diagnostics/triage. I am basically asking to push this part of the work on to the fuzzer. Otherwise, addressing random bugs doesn't scale. Triaging should have pointed to the root cause.

Now, there tends to be something to learn from bugs. In this case, the question was: "can we avoid constraints with duplications"? In particular, it points to a basic inefficiency of extracting conjunctions (and disjunctions). The function didn't deduplicate. So I added deduplication into this function. It is used throughout z3 code base so could expose latent issues. We will see.