diff --git a/liquidjava-verifier/pom.xml b/liquidjava-verifier/pom.xml
index 5b42f4cb..bcfa7079 100644
--- a/liquidjava-verifier/pom.xml
+++ b/liquidjava-verifier/pom.xml
@@ -95,7 +95,50 @@
 					</execution>
 				</executions>
 			</plugin>
+<plugin>
+<groupId>org.jacoco</groupId>
+<artifactId>jacoco-maven-plugin</artifactId>
+<version>0.8.14</version>
+<executions>
+<execution>
+<id>default-prepare-agent</id>
+<goals>
+<goal>prepare-agent</goal>
+</goals>
+</execution>
+<execution>
+<id>default-report</id>
+<goals>
+<goal>report</goal>
+</goals>
+</execution>
+<execution>
+<id>default-check</id>
+<goals>
+<goal>check</goal>
+</goals>
+<configuration>
+<rules>
+<rule>
+<element>BUNDLE</element>
+<limits>
+<limit>
+<counter>COMPLEXITY</counter>
+<value>COVEREDRATIO</value>
+<minimum>0.60</minimum>
+</limit>
+</limits>
+</rule>
+</rules>
+</configuration>
+</execution>
+</executions>
+</plugin>
+ 
+ 
 		</plugins>
+ 
+ 
 	</build>
 
 	<properties>
@@ -207,3 +250,4 @@
 		</dependencies>
 	</dependencyManagement>
 </project>
+
diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/BuiltinFunctionPredicate.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/BuiltinFunctionPredicate.java
new file mode 100644
index 00000000..62284b25
--- /dev/null
+++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/BuiltinFunctionPredicate.java
@@ -0,0 +1,33 @@
+package liquidjava.rj_language;
+
+import liquidjava.errors.ErrorEmitter;
+import liquidjava.rj_language.parsing.ParsingException;
+import spoon.reflect.declaration.CtElement;
+
+public class BuiltinFunctionPredicate extends Predicate {
+
+    public BuiltinFunctionPredicate(ErrorEmitter ee, CtElement elem, String functionName, String... params)
+            throws ParsingException {
+        super(functionName + "(" + getFormattedParams(params) + ")", elem, ee);
+    }
+
+    public static BuiltinFunctionPredicate builtin_length(String param, CtElement elem, ErrorEmitter ee)
+            throws ParsingException {
+        return new BuiltinFunctionPredicate(ee, elem, "length", param);
+    }
+
+    public static BuiltinFunctionPredicate builtin_addToIndex(String array, String index, String value, CtElement elem,
+            ErrorEmitter ee) throws ParsingException {
+        return new BuiltinFunctionPredicate(ee, elem, "addToIndex", index, value);
+    }
+
+    private static String getFormattedParams(String... params) {
+        StringBuilder sb = new StringBuilder();
+        for (int i = 0; i < params.length; i++) {
+            sb.append(params[i]);
+            if (i < params.length - 1)
+                sb.append(", ");
+        }
+        return sb.toString();
+    }
+}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/Predicate.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/Predicate.java
new file mode 100644
index 00000000..7fb7fa94
--- /dev/null
+++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/Predicate.java
@@ -0,0 +1,269 @@
+package liquidjava.rj_language;
+
+import java.util.ArrayList;
+import java.util.HashMap;
+import java.util.List;
+import java.util.Map;
+import java.util.stream.Collectors;
+import liquidjava.errors.ErrorEmitter;
+import liquidjava.errors.ErrorHandler;
+import liquidjava.processor.context.AliasWrapper;
+import liquidjava.processor.context.Context;
+import liquidjava.processor.context.GhostState;
+import liquidjava.processor.facade.AliasDTO;
+import liquidjava.rj_language.ast.BinaryExpression;
+import liquidjava.rj_language.ast.Expression;
+import liquidjava.rj_language.ast.FunctionInvocation;
+import liquidjava.rj_language.ast.GroupExpression;
+import liquidjava.rj_language.ast.Ite;
+import liquidjava.rj_language.ast.LiteralBoolean;
+import liquidjava.rj_language.ast.LiteralInt;
+import liquidjava.rj_language.ast.LiteralReal;
+import liquidjava.rj_language.ast.UnaryExpression;
+import liquidjava.rj_language.ast.Var;
+import liquidjava.rj_language.opt.derivation_node.DerivationNode;
+import liquidjava.rj_language.opt.derivation_node.ValDerivationNode;
+import liquidjava.rj_language.opt.ExpressionSimplifier;
+import liquidjava.rj_language.parsing.ParsingException;
+import liquidjava.rj_language.parsing.RefinementsParser;
+import liquidjava.utils.Utils;
+import spoon.reflect.declaration.CtElement;
+import spoon.reflect.declaration.CtType;
+import spoon.reflect.factory.Factory;
+
+/**
+ * Acts as a wrapper for Expression AST
+ *
+ * @author cgamboa
+ */
+public class Predicate {
+
+    protected Expression exp;
+    protected String prefix;
+
+    /** Create a predicate with the expression true */
+    public Predicate() {
+        exp = new LiteralBoolean(true);
+    }
+
+    /**
+     * Create a new predicate with a refinement
+     *
+     * @param ref
+     * @param element
+     * @param e
+     *
+     * @throws ParsingException
+     */
+    public Predicate(String ref, CtElement element, ErrorEmitter e) throws ParsingException {
+        this(ref, element, e, element.getParent(CtType.class).getQualifiedName());
+    }
+
+    /**
+     * Create a new predicate with a refinement and a given prefix for the class
+     * 
+     * @param ref
+     * @param element
+     * @param e
+     * @param prefix
+     * 
+     * @throws ParsingException
+     */
+    public Predicate(String ref, CtElement element, ErrorEmitter e, String prefix) throws ParsingException {
+        this.prefix = prefix;
+        exp = parse(ref, element, e);
+        if (e.foundError()) {
+            return;
+        }
+        if (!(exp instanceof GroupExpression)) {
+            exp = new GroupExpression(exp);
+        }
+    }
+
+    /** Create a predicate with the expression true */
+    public Predicate(Expression e) {
+        exp = e;
+    }
+
+    protected Expression parse(String ref, CtElement element, ErrorEmitter e) throws ParsingException {
+        try {
+            return RefinementsParser.createAST(ref, prefix);
+        } catch (ParsingException e1) {
+            ErrorHandler.printSyntaxError(e1.getMessage(), ref, element, e);
+            throw e1;
+        }
+    }
+
+    protected Expression innerParse(String ref, ErrorEmitter e, String prefix) {
+        try {
+            return RefinementsParser.createAST(ref, prefix);
+        } catch (ParsingException e1) {
+            ErrorHandler.printSyntaxError(e1.getMessage(), ref, e);
+        }
+        return null;
+    }
+
+    public Predicate changeAliasToRefinement(Context context, Factory f) throws Exception {
+        Expression ref = getExpression();
+
+        Map<String, AliasDTO> alias = new HashMap<>();
+        for (AliasWrapper aw : context.getAlias()) {
+            alias.put(aw.getName(), aw.createAliasDTO());
+        }
+
+        ref = ref.changeAlias(alias, context, f);
+        return new Predicate(ref);
+    }
+
+    public Predicate negate() {
+        return new Predicate(new UnaryExpression("!", exp));
+    }
+
+    public Predicate substituteVariable(String from, String to) {
+        Expression ec = exp.clone();
+        ec = ec.substitute(new Var(from), new Var(to));
+        return new Predicate(ec);
+    }
+
+    public List<String> getVariableNames() {
+        List<String> l = new ArrayList<>();
+        exp.getVariableNames(l);
+        return l;
+    }
+
+    public List<GhostState> getStateInvocations(List<GhostState> lgs) {
+        if (lgs == null)
+            return new ArrayList<>();
+        List<String> all = lgs.stream().map(p -> p.getQualifiedName()).collect(Collectors.toList());
+        List<String> toAdd = new ArrayList<>();
+        exp.getStateInvocations(toAdd, all);
+
+        List<GhostState> gh = new ArrayList<>();
+        for (String n : toAdd) {
+            for (GhostState g : lgs)
+                if (g.matches(n))
+                    gh.add(g);
+        }
+
+        return gh;
+    }
+
+    /** Change old mentions of previous name to the new name e.g., old(previousName) -> newName */
+    public Predicate changeOldMentions(String previousName, String newName, ErrorEmitter ee) {
+        Expression e = exp.clone();
+        Expression prev = createVar(previousName).getExpression();
+        List<Expression> le = new ArrayList<>();
+        le.add(createVar(newName).getExpression());
+        e.substituteFunction(Utils.OLD, le, prev);
+        return new Predicate(e);
+    }
+
+    public List<String> getOldVariableNames() {
+        List<String> ls = new ArrayList<>();
+        expressionGetOldVariableNames(this.exp, ls);
+        return ls;
+    }
+
+    private void expressionGetOldVariableNames(Expression exp, List<String> ls) {
+        if (exp instanceof FunctionInvocation) {
+            FunctionInvocation fi = (FunctionInvocation) exp;
+            if (fi.getName().equals(Utils.OLD)) {
+                List<Expression> le = fi.getArgs();
+                for (Expression e : le) {
+                    if (e instanceof Var)
+                        ls.add(((Var) e).getName());
+                }
+            }
+        }
+        if (exp.hasChildren()) {
+            for (var ch : exp.getChildren())
+                expressionGetOldVariableNames(ch, ls);
+        }
+    }
+
+    public Predicate changeStatesToRefinements(List<GhostState> ghostState, String[] toChange, ErrorEmitter ee) {
+        Map<String, Expression> nameRefinementMap = new HashMap<>();
+        for (GhostState gs : ghostState) {
+            if (gs.getRefinement() != null) { // is a state and not a ghost state
+                String name = gs.getQualifiedName();
+                Expression exp = innerParse(gs.getRefinement().toString(), ee, gs.getPrefix());
+                nameRefinementMap.put(name, exp);
+                // Also allow simple name lookup to enable hierarchy matching
+                String simple = Utils.getSimpleName(name);
+                nameRefinementMap.putIfAbsent(simple, exp);
+            }
+        }
+        Expression e = exp.substituteState(nameRefinementMap, toChange);
+        return new Predicate(e);
+    }
+
+    public boolean isBooleanTrue() {
+        return exp.isBooleanTrue();
+    }
+
+    @Override
+    public String toString() {
+        return exp.toString();
+    }
+
+    @Override
+    public Predicate clone() {
+        return new Predicate(exp.clone());
+    }
+
+    public Expression getExpression() {
+        return exp;
+    }
+
+    public ValDerivationNode simplify() {
+        return ExpressionSimplifier.simplify(exp.clone());
+    }
+
+    public static Predicate createConjunction(Predicate c1, Predicate c2) {
+        return new Predicate(new BinaryExpression(c1.getExpression(), Utils.AND, c2.getExpression()));
+    }
+
+    public static Predicate createDisjunction(Predicate c1, Predicate c2) {
+        return new Predicate(new BinaryExpression(c1.getExpression(), Utils.OR, c2.getExpression()));
+    }
+
+    public static Predicate createEquals(Predicate c1, Predicate c2) {
+        return new Predicate(new BinaryExpression(c1.getExpression(), Utils.EQ, c2.getExpression()));
+    }
+
+    public static Predicate createITE(Predicate c1, Predicate c2, Predicate c3) {
+        return new Predicate(new Ite(c1.getExpression(), c2.getExpression(), c3.getExpression()));
+    }
+
+    public static Predicate createLit(String value, String type) {
+        Expression ex;
+        if (type.equals(Utils.BOOLEAN))
+            ex = new LiteralBoolean(value);
+        else if (type.equals(Utils.INT))
+            ex = new LiteralInt(value);
+        else if (type.equals(Utils.DOUBLE))
+            ex = new LiteralReal(value);
+        else if (type.equals(Utils.SHORT))
+            ex = new LiteralInt(value);
+        else if (type.equals(Utils.LONG))
+            ex = new LiteralReal(value);
+        else // if(type.equals(Utils.DOUBLE))
+            ex = new LiteralReal(value);
+        return new Predicate(ex);
+    }
+
+    public static Predicate createOperation(Predicate c1, String op, Predicate c2) {
+        return new Predicate(new BinaryExpression(c1.getExpression(), op, c2.getExpression()));
+    }
+
+    public static Predicate createVar(String name) {
+        return new Predicate(new Var(name));
+    }
+
+    public static Predicate createInvocation(String name, Predicate... Predicates) {
+        List<Expression> le = new ArrayList<>();
+        for (Predicate c : Predicates)
+            le.add(c.getExpression());
+        return new Predicate(new FunctionInvocation(name, le));
+    }
+}
diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/TestLiteralString.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/TestLiteralString.java
new file mode 100644
index 00000000..7e82772f
--- /dev/null
+++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/TestLiteralString.java
@@ -0,0 +1,14 @@
+package liquidjava.rj_language;
+
+import static org.junit.Assert.assertNotEquals;
+import org.junit.Test;
+import liquidjava.rj_language.ast.LiteralString;
+
+public class TestLiteralString {
+    @Test
+    public void testLiteralString() {
+        LiteralString s1 = new LiteralString("hello");
+        LiteralString s2 = new LiteralString("world");
+        assertNotEquals(s1.hashCode(), s2.hashCode());
+    }
+}
diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/TestOptimization.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/TestOptimization.java
new file mode 100644
index 00000000..26f02e37
--- /dev/null
+++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/TestOptimization.java
@@ -0,0 +1,16 @@
+import static org.junit.Assert.assertEquals;
+import org.junit.Test;
+
+import liquidjava.rj_language.ast.BinaryExpression;
+import liquidjava.rj_language.ast.LiteralInt;
+import liquidjava.rj_language.opt.ConstantFolding;
+import liquidjava.rj_language.opt.derivation_node.ValDerivationNode;
+
+public class TestOptimization {
+    @Test
+    public void testBinaryFold() {
+        BinaryExpression b = new BinaryExpression(new LiteralInt(1), "+", new LiteralInt(2));
+        ValDerivationNode r = ConstantFolding.fold(new ValDerivationNode(b, null));
+        assertEquals(r.getValue(), new LiteralInt(3));
+    }
+}