Model translation failed for DefSet5 example
Description
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
Details
Assignee
Michael Leuschel
Michael LeuschelReporter
Michael Leuschel
Michael LeuschelPriority
Created November 11, 2020 at 8:54 PM
Updated November 12, 2020 at 8:37 AM
Resolved November 12, 2020 at 8:37 AM
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