Memory issue in BDDs. Probably related to arithmetic.

[Jonas Flament]

We noticed some strange behaviour while working on the Pacman project.

We added a new structure to test our refactored theory (which itself contains an unsat core when testing the huge structure).

When we try to generate models for it, it says it is unsatisfiable (with both the refactored theory as a working theory). Liftedunitpropagation and groundwithbounds have their default value.

When we try to print the unsat core, and turn of liftedunitpropagation and groundwithbounds as in the exercise session, we get an error that says it could find models, so it does not have an unsat core.

When we turn of liftedunitpropagation and groundwithbounds, and generate the models again, it can indeed generate models for it.

For easy testing, we include a zip with a makefile which automatically invokes idp.

The target 'auto-newstruct' will, automatically, test only the new structure. The target 'auto-all' will also automatically test our original solution, the corrected solution, and the refactored solution.

The makefile also includes comments with what happened when the target is run on the computers in the labs of 200 A.

NOTE: The makefile contains an IDP "variable" which points to the location of IDP program on the system. In the computer lab, this is /localhost/..../idp, but this should be changed when the IDP program is located elsewhere

[Bart Bogaerts]

Als bijlage een kleinere versie van deze issue.

Er gebeurt iets raar met memorydingen in de bdds: afhankelijk van de verbosity doet hij zich voor of niet.

TODO CHECKEN!