Approximatiefout in unsatcoreextraction

[Pieter Van Hertum]

Bij het uitvoeren van de modelexpansion op !x y z: P(x) & P(y) & P(z) => z=y | z=x. Met structuur P={a;b}, krijgen we geen model, maar bij het opvragen van een unsatcore krijgen we wel "Error: The given theory has models that extend the structure, so there are no unsat cores."

Het uitzetten van de approximatie lost dit probleem op.

[Bart Bogaerts]

oplossing (zie pullrequest UC)

UC should check the structure If approximation already derives one marker to be true. That clause is unsat in structure.

[Broes De Cat]

UC pull request zat er al bij...

[Pieter Van Hertum]

allerlaatste versie van de master heeft inderdaad nog altijd zelfde probleem