Z3-model: more restrictions on constant arrays.
@@ -137,8 +137,11 @@ class Z3Model extends CachingAbstractModel<Long, Long, Long> {
return getArrayAssignments(symbol, arrayFormula, value, Collections.emptyList());
} else if (Native.isApp(z3context, value) && 1 == Native.getAppNumArgs(z3context, value)) {
+ long decl = Native.getAppDecl(z3context, value);
+ long name = Native.getDeclName(z3context, decl);
+ if ("const".equals(Native.getSymbolString(z3context, name))) {
// Sometimes we get an array of zeros as "((as const (Array Int Int)) 0)".
- // We return the plain value with no argumentInterpretations, as assignment "arr[*] = 0",
+ // We return the plain value with no argumentInterpretations, as assignment "arr = 0",
// because there is no better way of modeling a whole array.
return Collections.singletonList(
new ValueAssignment(
@@ -146,11 +149,11 @@ class Z3Model extends CachingAbstractModel<Long, Long, Long> {
z3creator.symbolToString(symbol),
z3creator.convertValue(Native.getAppArg(z3context, value, 0)),
ImmutableList.of()));
+ }
+ }
- } else {
throw new UnsupportedOperationException(
"unknown model evaluation: " + Native.astToString(z3context, value));
- }
} finally {
// cleanup outdated data
