File tree Expand file tree Collapse file tree 3 files changed +0
-5
lines changed
liquidjava-verifier/src/main/java/liquidjava
processor/refinement_checker Expand file tree Collapse file tree 3 files changed +0
-5
lines changed Original file line number Diff line number Diff line change 99import liquidjava .diagnostics .errors .*;
1010import liquidjava .processor .context .AliasWrapper ;
1111import liquidjava .processor .context .Context ;
12- import liquidjava .processor .context .ContextHistory ;
1312import liquidjava .processor .context .GhostFunction ;
1413import liquidjava .processor .context .GhostState ;
1514import liquidjava .processor .context .RefinedVariable ;
@@ -41,7 +40,6 @@ public abstract class TypeChecker extends CtScanner {
4140 protected final Context context ;
4241 protected final Factory factory ;
4342 protected final VCChecker vcChecker ;
44- private final ContextHistory contextHistory = ContextHistory .getInstance ();
4543
4644 public TypeChecker (Context context , Factory factory ) {
4745 this .context = context ;
Original file line number Diff line number Diff line change 66import java .util .Map ;
77import java .util .stream .Collectors ;
88
9- import liquidjava .diagnostics .errors .ArgumentMismatchError ;
109import liquidjava .diagnostics .errors .LJError ;
11- import liquidjava .diagnostics .errors .SyntaxError ;
1210import liquidjava .processor .context .AliasWrapper ;
1311import liquidjava .processor .context .Context ;
1412import liquidjava .processor .context .GhostFunction ;
Original file line number Diff line number Diff line change 66import com .microsoft .z3 .Expr ;
77import com .microsoft .z3 .FPExpr ;
88import com .microsoft .z3 .FuncDecl ;
9- import com .microsoft .z3 .FuncInterp ;
109import com .microsoft .z3 .IntExpr ;
1110import com .microsoft .z3 .IntNum ;
1211import com .microsoft .z3 .RealExpr ;
You can’t perform that action at this time.
0 commit comments