@@ -50,7 +50,8 @@ public TranslatorToZ3(liquidjava.processor.context.Context context) {
5050 TranslatorContextToZ3 .addAliases (context .getAliases (), aliasTranslation );
5151 TranslatorContextToZ3 .addGhostFunctions (z3 , context .getGhosts (), funcTranslation );
5252 TranslatorContextToZ3 .addGhostStates (z3 , context .getGhostStates (), funcTranslation );
53- instanceVariableRefinements = context .getCtxInstanceVars ().stream ().map (v -> v .getRefinement ().toString ()).collect (Collectors .toSet ());
53+ instanceVariableRefinements = context .getCtxInstanceVars ().stream ().map (v -> v .getRefinement ().toString ())
54+ .collect (Collectors .toSet ());
5455 }
5556
5657 @ SuppressWarnings ("unchecked" )
@@ -72,7 +73,8 @@ public Counterexample getCounterexample(Model model) {
7273 Expr <?> value = model .getConstInterp (decl );
7374 String assignment = name + " == " + value ;
7475 // Skip values of uninterpreted sorts
75- if (value .getSort ().getSortKind () != Z3_sort_kind .Z3_UNINTERPRETED_SORT && !instanceVariableRefinements .contains (assignment ))
76+ if (value .getSort ().getSortKind () != Z3_sort_kind .Z3_UNINTERPRETED_SORT
77+ && !instanceVariableRefinements .contains (assignment ))
7678 assignments .add (assignment );
7779 }
7880 }
@@ -84,7 +86,7 @@ public Counterexample getCounterexample(Model model) {
8486 String assignment = name + " == " + value ;
8587 if (!instanceVariableRefinements .contains (assignment ))
8688 assignments .add (assignment );
87- }
89+ }
8890 return new Counterexample (assignments );
8991 }
9092
0 commit comments