Soundness bug in z3str3

[numairmansur]

Hi @mtrberzi
On the latest commit (1aea0d2), I get the following wrong result on the following satisfiable file:

65.zip

sat
sat
unsat

I didn't exactly check on which commit was this bug introduced but I think it was introduced recently.

[numairmansur]

On commit 321bad2, i correctly get

sat
sat
sat

[mtrberzi]

You're right that this was introduced recently, setting smt.str.fixed_length_models=false prevents the bug so that should narrow it down.

[mtrberzi]

This also suddenly starts working if I take out the first (push 3) command.

[mtrberzi]

Something very strange is going on as calling (check-sat) twice in a row with nothing in between produces a sat followed by an unsat.

[mtrberzi]

I'm ultimately not sure which internal data structure was causing the problem, but cleaning them all up between runs is probably not a bad idea, and that fixed this completely. Opened #3818.

[numairmansur]

awesome. Thanks !