diff --git a/liquidjava-example/src/main/java/testSuite/classes/bytebuf_correct/ByteBufferRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/bytebuf_correct/ByteBufferRefinements.java
index e18e7deec..ea45d91e6 100644
--- a/liquidjava-example/src/main/java/testSuite/classes/bytebuf_correct/ByteBufferRefinements.java
+++ b/liquidjava-example/src/main/java/testSuite/classes/bytebuf_correct/ByteBufferRefinements.java
@@ -3,18 +3,9 @@
 import liquidjava.specification.ExternalRefinementsFor;
 import liquidjava.specification.Ghost;
 import liquidjava.specification.Refinement;
-import liquidjava.specification.RefinementAlias;
 import liquidjava.specification.StateRefinement;
-import liquidjava.specification.StateSet;
 
 import java.nio.ByteBuffer;
-import java.nio.ByteOrder;
-import java.nio.CharBuffer;
-import java.nio.ShortBuffer;
-import java.nio.IntBuffer;
-import java.nio.LongBuffer;
-import java.nio.FloatBuffer;
-import java.nio.DoubleBuffer;
 
 
 @Ghost("boolean arrayBacked")
diff --git a/liquidjava-example/src/main/java/testSuite/classes/bytebuf_error/ByteBufferRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/bytebuf_error/ByteBufferRefinements.java
index c3e056024..3bae0b510 100644
--- a/liquidjava-example/src/main/java/testSuite/classes/bytebuf_error/ByteBufferRefinements.java
+++ b/liquidjava-example/src/main/java/testSuite/classes/bytebuf_error/ByteBufferRefinements.java
@@ -3,18 +3,9 @@
 import liquidjava.specification.ExternalRefinementsFor;
 import liquidjava.specification.Ghost;
 import liquidjava.specification.Refinement;
-import liquidjava.specification.RefinementAlias;
 import liquidjava.specification.StateRefinement;
-import liquidjava.specification.StateSet;
 
 import java.nio.ByteBuffer;
-import java.nio.ByteOrder;
-import java.nio.CharBuffer;
-import java.nio.ShortBuffer;
-import java.nio.IntBuffer;
-import java.nio.LongBuffer;
-import java.nio.FloatBuffer;
-import java.nio.DoubleBuffer;
 
 
 @Ghost("boolean arrayBacked")
diff --git a/liquidjava-example/src/main/java/testSuite/classes/iterator_queue_error/IteratorRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/iterator_queue_error/IteratorRefinements.java
index 3af73c39f..e6d335e63 100644
--- a/liquidjava-example/src/main/java/testSuite/classes/iterator_queue_error/IteratorRefinements.java
+++ b/liquidjava-example/src/main/java/testSuite/classes/iterator_queue_error/IteratorRefinements.java
@@ -1,7 +1,6 @@
 package testSuite.classes.iterator_queue_error;
 
 import liquidjava.specification.ExternalRefinementsFor;
-import liquidjava.specification.Refinement;
 import liquidjava.specification.StateRefinement;
 import liquidjava.specification.StateSet;
 
diff --git a/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_correct/PreparedStatementRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_correct/PreparedStatementRefinements.java
index ce33d6a57..aaccee280 100644
--- a/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_correct/PreparedStatementRefinements.java
+++ b/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_correct/PreparedStatementRefinements.java
@@ -1,13 +1,10 @@
 package testSuite.classes.resultset_forward_correct;
 
 import java.sql.ResultSet;
-import java.sql.SQLException;
 
 import liquidjava.specification.ExternalRefinementsFor;
 import liquidjava.specification.Ghost;
 import liquidjava.specification.Refinement;
-import liquidjava.specification.StateRefinement;
-import liquidjava.specification.StateSet;
 
 
 @Ghost("boolean setBackwards")
diff --git a/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_error/PreparedStatementRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_error/PreparedStatementRefinements.java
index 27f6446e3..d4aadbd52 100644
--- a/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_error/PreparedStatementRefinements.java
+++ b/liquidjava-example/src/main/java/testSuite/classes/resultset_forward_error/PreparedStatementRefinements.java
@@ -1,13 +1,10 @@
 package testSuite.classes.resultset_forward_error;
 
 import java.sql.ResultSet;
-import java.sql.SQLException;
 
 import liquidjava.specification.ExternalRefinementsFor;
 import liquidjava.specification.Ghost;
 import liquidjava.specification.Refinement;
-import liquidjava.specification.StateRefinement;
-import liquidjava.specification.StateSet;
 
 
 @Ghost("boolean setBackwards")
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java
index 78b5e0aad..ec604957d 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java
@@ -5,7 +5,6 @@
 import java.util.stream.Collectors;
 
 import liquidjava.diagnostics.TranslationTable;
-import liquidjava.processor.VCImplication;
 import liquidjava.rj_language.Predicate;
 import liquidjava.rj_language.ast.Expression;
 import liquidjava.rj_language.ast.formatter.VariableFormatter;
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java
index 581b46443..3dda3881b 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java
@@ -7,9 +7,7 @@
 import liquidjava.diagnostics.errors.LJError;
 import liquidjava.processor.context.Context;
 import liquidjava.processor.refinement_checker.general_checkers.MethodsFunctionsChecker;
-import liquidjava.rj_language.Predicate;
 import liquidjava.utils.constants.Formats;
-import liquidjava.utils.constants.Types;
 import spoon.reflect.declaration.CtClass;
 import spoon.reflect.declaration.CtConstructor;
 import spoon.reflect.declaration.CtEnum;
diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java
index ff69881ca..696ef5eb9 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java
@@ -6,11 +6,8 @@
 import java.util.Map;
 import java.util.stream.Collectors;
 
-import liquidjava.diagnostics.DebugLog;
 import liquidjava.diagnostics.errors.LJError;
 import liquidjava.diagnostics.errors.NotFoundError;
-import liquidjava.processor.VCImplication;
-import liquidjava.rj_language.opt.VCSimplificationResult;
 import liquidjava.processor.context.AliasWrapper;
 import liquidjava.processor.context.Context;
 import liquidjava.processor.context.GhostFunction;
diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplificationResult.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplificationResult.java
index 6f35822d0..d70b2a774 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplificationResult.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplificationResult.java
@@ -1,7 +1,5 @@
 package liquidjava.rj_language.opt;
 
-import java.util.Objects;
-
 import liquidjava.processor.VCImplication;
 
 /**
diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java
index 981f5a138..8eb366eaf 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java
@@ -3,7 +3,6 @@
 import com.microsoft.z3.ArithExpr;
 import com.microsoft.z3.ArrayExpr;
 import com.microsoft.z3.BoolExpr;
-import com.microsoft.z3.EnumSort;
 import com.microsoft.z3.Expr;
 import com.microsoft.z3.FPExpr;
 import com.microsoft.z3.FuncDecl;