Model translation failed for DefSet5 example

Description

For this example

MACHINE DefSet5 DEFINITIONS SET_PREF_MAX_INITIALISATIONS == 73; SETS ID PROPERTIES card(ID) = 5 END

we get this error:

>>> :z3 (ID=P1\/P2) & (P1/\P2={}) & (aa/=bb) & ({aa,bb,xx}<:ID) & (card(ID)=5) & (aa:P1) & (bb:P2) & (xx:P2) & (xx/=bb) & (card(P1)=1) & not((aa:P1) & (bb:P2) & (xx:P2) & (xx=bb) & (card(P1)=1)) ! Missing translation for Z3 expression: [store,[store,[store,[...|...]|...],'ID!val!2'|...],'ID!val!3',false]:set(global('ID')) Unknown exception in solver z3: model_translation_failed PREDICATE is UNKNOWN: model_translation_failed

Environment

None

Activity

Show:

Michael Leuschel November 12, 2020 at 8:36 AM

There were two problems here: a missing translation for store … false and the fact that as const Array Type Bool ignored the Type and always returned BOOL.

 

Test 2063 was added and problem is now fixed in commit 8647e76ac15c7f5dedf26ebc772b5457a02110c1

Fixed

Details

Assignee

Reporter

Priority

Created November 11, 2020 at 8:54 PM
Updated November 12, 2020 at 8:37 AM
Resolved November 12, 2020 at 8:37 AM