valid_assignment() assertion violation

[daniel-j-h]

To get a better feeing for z3 I wanted to do constraint-based layouting.
https://gist.github.com/daniel-j-h/499c50455929ab6aa755

Surprisingly though, I stumbled upon a strange assertion.
This is triggered only when I set the enclosing box to a resolution of 1366,768 and use the area function (i.e. multiplication). Setting the box to 1365,768 or switching the area constraint with width and height constraints does give me a valid model.

ASSERTION VIOLATION
File: ../src/smt/theory_arith_aux.h
Line: 1996
valid_assignment()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
A

I could only trace it back to theory_arith_inv.h's valid_assignment, and then satisfy_integrality. I can see no reason why this assertion could happen. Would you be so kind and have a look at it? Is the multiplication the problem? As far as I read the Ints theory spec, there is an (* Int Int Int :left-assoc) symbol.

This is tested with

Z3 [version 4.4.0 - 64 bit - build hashcode bd162588b28c1ca38980bfd0df040539df176370].

and also with the latest (as of now)

Z3 [version 4.4.0 - 64 bit - build hashcode 3ba2e712b21bb5c8e987243c118adbd8b30b185d]

Thanks,
Daniel

[daniel-j-h]

I am unable to reproduce this with latest versions of unstable (or opt)

You are right, with the latest opt branch I do not get the assertion. Closing this. Thanks for your help.