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

Michael Leuschel

Reporter

Michael Leuschel

Priority

Major

Created November 11, 2020 at 8:54 PM

Updated November 12, 2020 at 8:37 AM

Resolved November 12, 2020 at 8:37 AM

Configure