Solver returns valid example as counter-example

[palas]

When testing this implementation of symbolic sets using the master of Z3 as of commit 04e6e0b, I get the following output in ghci:

*FSSet> proveWith z3{validateModel = True} (\x y l -> FSSet.valid 10 l .=> (FSSet.elem 12 (x :: SInteger) (FSSet.insert 12 y (FSSet.insert 12 x l))))
*** Data.SBV: Model validation failure: Counter-example violates no constraints.
*** 
*** Assignment:
*** 
***       s0 =                                      1728 :: Integer
***       s1 =                                      1729 :: Integer
***       s2 = [1724,1725,1726,1727,1730,1731,1732,1733] :: [Integer]
*** 
*** Backend solver returned a model that does not satisfy the constraints.
*** This could indicate a bug in the backend solver, or SBV itself. Please report.
***
*** Alleged model:
***
*** Falsifiable. Counter-example:
***   s0 =                                      1728 :: Integer
***   s1 =                                      1729 :: Integer
***   s2 = [1724,1725,1726,1727,1730,1731,1732,1733] :: [Integer]

[LeventErkok]

Thanks. this is definitely an issue; and I suspect it might be z3's fault. Though it needs to be debugged. Any chance you can find a "smaller" instance?

By smaller, I mean the following. If you run with:

  proveWith z3{verbose=True}

SBV will print what it sends to the solver. The shorter that trace, the better.

[palas]

For now I made it a bit smaller by removing one insert:

proveWith z3{validateModel = True} (\x y l -> ((Data.SBV.List.elem x l) .&& (FSSet.valid 8 l)) .=> (FSSet.elem 9 (x :: SInteger) (FSSet.insert 9 (y :: SInteger) l)))

[LeventErkok]

Thanks! That helps; though it'd be great to shrink it further. Eventually, if we determine this is an issue with z3, we'll file it as a bug report with z3 folks with the generated trace; and it'd be really hard for them to decipher what's wrong. There must be a reason why it's failing and if we can precisely identify the root cause, I trust we might be able to find a much shorter trace. I'll be looking into it as well, but you have the best insight into the problem, so I'm hoping you'll get there before I do!

[LeventErkok]

@palas

Filed an issue with z3: Z3Prover/z3#2445

They're quite responsive to bug reports, so I expect they'll fix this upstream quite soon.

[LeventErkok]

@palas This is now working just fine with the latest z3!