diff --git a/.travis.yml b/.travis.yml
index 4651be32..1d840f3f 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -1,5 +1,13 @@
+sudo: required
+dist: trusty
+
+services: docker
+
 language: java
 
 script:
- - ant;
- - ant test;
+ - docker-compose up --build -d
+ - docker ps -a
+
+after_script:
+ - docker-compose down
diff --git a/.travis.yml.swp b/.travis.yml.swp
new file mode 100644
index 00000000..4e5923e2
Binary files /dev/null and b/.travis.yml.swp differ
diff --git a/Dockerfile b/Dockerfile
index e465a44f..46ebc64c 100644
--- a/Dockerfile
+++ b/Dockerfile
@@ -15,7 +15,7 @@ RUN apt install patchelf -y
 RUN apt install libgomp1
 
 # Clone down the GreenSolver repository
-RUN git clone https://github.com/wvisser/green
+RUN git clone https://github.com/marcdefaria/green
 
 # Download and extract Z3
 RUN mkdir z3
@@ -35,3 +35,7 @@ RUN mv z3-4.7.1-x64-ubuntu-16.04/ z3/
 WORKDIR /green/
 RUN sed -i '16s/.*/z3path = \/z3\/z3\/bin\/z3/' build.properties
 RUN sed -i '17s/.*/z3lib = \/z3\/z3\/bin/' build.properties
+
+#run the test
+RUN ant
+RUN ant test
diff --git a/README.md b/README.md
index aedc3ddc..0b682bb2 100644
--- a/README.md
+++ b/README.md
@@ -1,7 +1,7 @@
-[![Build Status](https://travis-ci.org/wvisser/green.svg?branch=master)](https://travis-ci.org/wvisser/green.svg?branch=master)
+[![Build Status](https://travis-ci.org/marcdefaria/green.svg?branch=master)](https://travis-ci.org/marcdefaria/green)
 
 Notes:
-
+HvQSDNw9jQZYGx6mw8N0Bg
 The first step is to update "build.properties" with your local
 settings.  You do not need to set z3 and latte, but in that case
 some unit tests won't run.
diff --git a/build.xml b/build.xml
index 0c29bed8..46321a09 100644
--- a/build.xml
+++ b/build.xml
@@ -95,8 +95,8 @@
     <target name="test">
     	<echo message="java.library.path = ${z3lib};${cvc3lib}"/>
         <mkdir dir="${junit.dir}"/>
-        <junit fork="yes" printsummary="withOutAndErr" haltonfailure = "yes">
-            <formatter type="xml"/>
+        <junit fork="yes" printsummary="yes" haltonfailure = "yes" showoutput="true">
+            <formatter type="plain" usefile="false"/>
             <test name="za.ac.sun.cs.green.EntireSuite" todir="${junit.dir}"/>
             <env key="DYLD_LIBRARY_PATH" value="lib"/>
             <env key="LD_LIBRARY_PATH" value="lib"/>
@@ -108,7 +108,7 @@
                 <include name="TEST-*.xml"/>
             </fileset>
             <report format="frames" todir="${junit.dir}"/>
-        </junitreport>
+        </junitreport>		
     </target>
 
 <!--
diff --git a/docker-compose.yml b/docker-compose.yml
new file mode 100644
index 00000000..11c099f5
--- /dev/null
+++ b/docker-compose.yml
@@ -0,0 +1,10 @@
+version: '2'
+services:
+  web:
+    build: .
+    ports:
+     - "5000:5000"
+    volumes:
+     - .:/code
+  redis:
+    image: "redis:alpine"
diff --git a/src/za/ac/sun/cs/green/service/simplify/ConstantPropogation.java b/src/za/ac/sun/cs/green/service/simplify/ConstantPropogation.java
new file mode 100644
index 00000000..d29e3b94
--- /dev/null
+++ b/src/za/ac/sun/cs/green/service/simplify/ConstantPropogation.java
@@ -0,0 +1,682 @@
+package za.ac.sun.cs.green.service.canonizer;
+
+import java.util.Collections;
+import java.util.HashMap;
+import java.util.Map;
+import java.util.Set;
+import java.util.SortedMap;
+import java.util.SortedSet;
+import java.util.Stack;
+import java.util.TreeMap;
+import java.util.TreeSet;
+import java.util.logging.Level;
+
+import za.ac.sun.cs.green.Instance;
+import za.ac.sun.cs.green.Green;
+import za.ac.sun.cs.green.expr.Expression;
+import za.ac.sun.cs.green.service.BasicService;
+import za.ac.sun.cs.green.util.Reporter;
+import za.ac.sun.cs.green.expr.Constant;
+import za.ac.sun.cs.green.expr.IntConstant;
+import za.ac.sun.cs.green.expr.IntVariable;
+import za.ac.sun.cs.green.expr.Operation;
+import za.ac.sun.cs.green.expr.Variable;
+import za.ac.sun.cs.green.expr.Visitor;
+import za.ac.sun.cs.green.expr.VisitorException;
+
+public class ConstantPropogation extends BasicService {
+
+	/**
+	 * Number of times the slicer has been invoked.
+	 */
+	private int invocations = 0;
+
+	public ConstantPropogation(Green solver) {
+		super(solver);
+	}
+
+	@Override
+	public Set<Instance> processRequest(Instance instance) {
+		@SuppressWarnings("unchecked")
+		Set<Instance> result = (Set<Instance>) instance.getData(getClass());
+		if (result == null) {
+			final Map<Variable, Variable> map = new HashMap<Variable, Variable>();
+			final Expression e = canonize(instance.getFullExpression(), map);
+			final Instance i = new Instance(getSolver(), instance.getSource(), null, e);
+			result = Collections.singleton(i);
+			instance.setData(getClass(), result);
+		}
+		return result;
+	}
+
+	@Override
+	public void report(Reporter reporter) {
+		reporter.report(getClass().getSimpleName(), "invocations = " + invocations);
+	}
+
+	public Expression canonize(Expression expression,
+			Map<Variable, Variable> map) {
+		try {
+			log.log(Level.FINEST, "Before Canonization: " + expression);
+			invocations++;
+			OrderingVisitor orderingVisitor = new OrderingVisitor();
+			expression.accept(orderingVisitor);
+			expression = orderingVisitor.getExpression();
+			CanonizationVisitor canonizationVisitor = new CanonizationVisitor();
+			expression.accept(canonizationVisitor);
+			Expression canonized = canonizationVisitor.getExpression();
+			if (canonized != null) {
+				canonized = new Renamer(map,
+						canonizationVisitor.getVariableSet()).rename(canonized);
+			}
+			log.log(Level.FINEST, "After Canonization: " + canonized);
+			return canonized;
+		} catch (VisitorException x) {
+			log.log(Level.SEVERE,
+					"encountered an exception -- this should not be happening!",
+					x);
+		}
+		return null;
+	}
+
+	private static class OrderingVisitor extends Visitor {
+
+		private Stack<Expression> stack;
+
+		public OrderingVisitor() {
+			stack = new Stack<Expression>();
+		}
+
+		public Expression getExpression() {
+			return stack.pop();
+		}
+
+		@Override
+		public void postVisit(IntConstant constant) {
+			stack.push(constant);
+		}
+
+		@Override
+		public void postVisit(IntVariable variable) {
+			stack.push(variable);
+		}
+
+		@Override
+		public void postVisit(Operation operation) throws VisitorException {
+			Operation.Operator op = operation.getOperator();
+			Operation.Operator nop = null;
+			switch (op) {
+			case EQ:
+				nop = Operation.Operator.EQ;
+				break;
+			case NE:
+				nop = Operation.Operator.NE;
+				break;
+			case LT:
+				nop = Operation.Operator.GT;
+				break;
+			case LE:
+				nop = Operation.Operator.GE;
+				break;
+			case GT:
+				nop = Operation.Operator.LT;
+				break;
+			case GE:
+				nop = Operation.Operator.LE;
+				break;
+			default:
+				break;
+			}
+			if (nop != null) {
+				Expression r = stack.pop();
+				Expression l = stack.pop();
+				if ((r instanceof IntVariable)
+						&& (l instanceof IntVariable)
+						&& (((IntVariable) r).getName().compareTo(
+								((IntVariable) l).getName()) < 0)) {
+					stack.push(new Operation(nop, r, l));
+				} else if ((r instanceof IntVariable)
+						&& (l instanceof IntConstant)) {
+					stack.push(new Operation(nop, r, l));
+				} else {
+					stack.push(operation);
+				}
+			} else if (op.getArity() == 2) {
+				Expression r = stack.pop();
+				Expression l = stack.pop();
+				stack.push(new Operation(op, l, r));
+			} else {
+				for (int i = op.getArity(); i > 0; i--) {
+					stack.pop();
+				}
+				stack.push(operation);
+			}
+		}
+
+	}
+
+	private static class CanonizationVisitor extends Visitor {
+
+		private Stack<Expression> stack;
+
+		private SortedSet<Expression> conjuncts;
+
+		private SortedSet<IntVariable> variableSet;
+
+		private Map<IntVariable, Integer> lowerBounds;
+
+		private Map<IntVariable, Integer> upperBounds;
+
+		private IntVariable boundVariable;
+
+		private Integer bound;
+
+		private int boundCoeff;
+
+		private boolean unsatisfiable;
+
+		private boolean linearInteger;
+
+		public CanonizationVisitor() {
+			stack = new Stack<Expression>();
+			conjuncts = new TreeSet<Expression>();
+			variableSet = new TreeSet<IntVariable>();
+			unsatisfiable = false;
+			linearInteger = true;
+		}
+
+		public SortedSet<IntVariable> getVariableSet() {
+			return variableSet;
+		}
+
+		public Expression getExpression() {
+			if (!linearInteger) {
+				return null;
+			} else if (unsatisfiable) {
+				return Operation.FALSE;
+			} else {
+				if (!stack.isEmpty()) {
+					Expression x = stack.pop();
+					if (x.equals(Operation.FALSE)) {
+						return Operation.FALSE;
+					} else if (!x.equals(Operation.TRUE)) {
+						conjuncts.add(x);
+					}
+				}
+				SortedSet<Expression> newConjuncts = processBounds();
+//				new TreeSet<Expression>();
+				Expression c = null;
+				for (Expression e : newConjuncts) {
+					if (e.equals(Operation.FALSE)) {
+						return Operation.FALSE;
+					} else if (e instanceof Operation) {
+						Operation o = (Operation) e;
+						if (o.getOperator() == Operation.Operator.GT) {
+							e = new Operation(Operation.Operator.LT, scale(-1,
+									o.getOperand(0)), o.getOperand(1));
+						} else if (o.getOperator() == Operation.Operator.GE) {
+							e = new Operation(Operation.Operator.LE, scale(-1,
+									o.getOperand(0)), o.getOperand(1));
+						}
+						o = (Operation) e;
+						if (o.getOperator() == Operation.Operator.GT) {
+							e = new Operation(Operation.Operator.GE, merge(
+									o.getOperand(0), new IntConstant(-1)),
+									o.getOperand(1));
+						} else if (o.getOperator() == Operation.Operator.LT) {
+							e = new Operation(Operation.Operator.LE, merge(
+									o.getOperand(0), new IntConstant(1)),
+									o.getOperand(1));
+						}
+					}
+					if (c == null) {
+						c = e;
+					} else {
+						c = new Operation(Operation.Operator.AND, c, e);
+					}
+				}
+				return (c == null) ? Operation.TRUE : c;
+			}
+		}
+
+		private SortedSet<Expression> processBounds() {
+			return conjuncts;
+		}
+
+		@SuppressWarnings("unused")
+		private void extractBound(Expression e) throws VisitorException {
+			if (e instanceof Operation) {
+				Operation o = (Operation) e;
+				Expression lhs = o.getOperand(0);
+				Operation.Operator op = o.getOperator();
+				if (isBound(lhs)) {
+					switch (op) {
+					case EQ:
+						lowerBounds.put(boundVariable, bound * boundCoeff);
+						upperBounds.put(boundVariable, bound * boundCoeff);
+						break;
+					case LT:
+						if (boundCoeff == 1) {
+							upperBounds.put(boundVariable, bound * -1 - 1);
+						} else {
+							lowerBounds.put(boundVariable, bound + 1);
+						}
+						break;
+					case LE:
+						if (boundCoeff == 1) {
+							upperBounds.put(boundVariable, bound * -1);
+						} else {
+							lowerBounds.put(boundVariable, bound);
+						}
+						break;
+					case GT:
+						if (boundCoeff == 1) {
+							lowerBounds.put(boundVariable, bound * -1 + 1);
+						} else {
+							upperBounds.put(boundVariable, bound - 1);
+						}
+						break;
+					case GE:
+						if (boundCoeff == 1) {
+							lowerBounds.put(boundVariable, bound * -1);
+						} else {
+							upperBounds.put(boundVariable, bound);
+						}
+						break;
+					default:
+						break;
+					}
+				}
+			}
+		}
+
+		private boolean isBound(Expression lhs) {
+			if (!(lhs instanceof Operation)) {
+				return false;
+			}
+			Operation o = (Operation) lhs;
+			if (o.getOperator() == Operation.Operator.MUL) {
+				if (!(o.getOperand(0) instanceof IntConstant)) {
+					return false;
+				}
+				if (!(o.getOperand(1) instanceof IntVariable)) {
+					return false;
+				}
+				boundVariable = (IntVariable) o.getOperand(1);
+				bound = 0;
+				if ((((IntConstant) o.getOperand(0)).getValue() == 1)
+						|| (((IntConstant) o.getOperand(0)).getValue() == -1)) {
+					boundCoeff = ((IntConstant) o.getOperand(0)).getValue();
+					return true;
+				} else {
+					return false;
+				}
+			} else if (o.getOperator() == Operation.Operator.ADD) {
+				if (!(o.getOperand(1) instanceof IntConstant)) {
+					return false;
+				}
+				bound = ((IntConstant) o.getOperand(1)).getValue();
+				if (!(o.getOperand(0) instanceof Operation)) {
+					return false;
+				}
+				Operation p = (Operation) o.getOperand(0);
+				if (!(p.getOperand(0) instanceof IntConstant)) {
+					return false;
+				}
+				if (!(p.getOperand(1) instanceof IntVariable)) {
+					return false;
+				}
+				boundVariable = (IntVariable) p.getOperand(1);
+				if ((((IntConstant) p.getOperand(0)).getValue() == 1)
+						|| (((IntConstant) p.getOperand(0)).getValue() == -1)) {
+					boundCoeff = ((IntConstant) p.getOperand(0)).getValue();
+					return true;
+				} else {
+					return false;
+				}
+			} else {
+				return false;
+			}
+		}
+
+		@Override
+		public void postVisit(Constant constant) {
+			if (linearInteger && !unsatisfiable) {
+				if (constant instanceof IntConstant) {
+					stack.push(constant);
+				} else {
+					stack.clear();
+					linearInteger = false;
+				}
+			}
+		}
+
+		@Override
+		public void postVisit(Variable variable) {
+			if (linearInteger && !unsatisfiable) {
+				if (variable instanceof IntVariable) {
+					variableSet.add((IntVariable) variable);
+					stack.push(new Operation(Operation.Operator.MUL, Operation.ONE,
+							variable));
+				} else {
+					stack.clear();
+					linearInteger = false;
+				}
+			}
+		}
+
+		@Override
+		public void postVisit(Operation operation) throws VisitorException {
+			if (!linearInteger || unsatisfiable) {
+				return;
+			}
+			Operation.Operator op = operation.getOperator();
+			switch (op) {
+			case AND:
+				if (!stack.isEmpty()) {
+					Expression x = stack.pop();
+					if (!x.equals(Operation.TRUE)) {
+						conjuncts.add(x);
+					}
+				}
+				if (!stack.isEmpty()) {
+					Expression x = stack.pop();
+					if (!x.equals(Operation.TRUE)) {
+						conjuncts.add(x);
+					}
+				}
+				break;
+			case EQ:
+			case NE:
+			case LT:
+			case LE:
+			case GT:
+			case GE:
+				if (!stack.isEmpty()) {
+					Expression e = merge(scale(-1, stack.pop()), stack.pop());
+					if (e instanceof IntConstant) {
+						int v = ((IntConstant) e).getValue();
+						boolean b = true;
+						if (op == Operation.Operator.EQ) {
+							b = v == 0;
+						} else if (op == Operation.Operator.NE) {
+							b = v != 0;
+						} else if (op == Operation.Operator.LT) {
+							b = v < 0;
+						} else if (op == Operation.Operator.LE) {
+							b = v <= 0;
+						} else if (op == Operation.Operator.GT) {
+							b = v > 0;
+						} else if (op == Operation.Operator.GE) {
+							b = v >= 0;
+						}
+						if (b) {
+							stack.push(Operation.TRUE);
+						} else {
+							stack.push(Operation.FALSE);
+							// unsatisfiable = true;
+						}
+					} else {
+						stack.push(new Operation(op, e, Operation.ZERO));
+					}
+				}
+				break;
+			case ADD:
+				stack.push(merge(stack.pop(), stack.pop()));
+				break;
+			case SUB:
+				stack.push(merge(scale(-1, stack.pop()), stack.pop()));
+				break;
+			case MUL:
+				if (stack.size() >= 2) {
+					Expression r = stack.pop();
+					Expression l = stack.pop();
+					if ((l instanceof IntConstant) && (r instanceof IntConstant)) {
+						int li = ((IntConstant) l).getValue();
+						int ri = ((IntConstant) r).getValue();
+						stack.push(new IntConstant(li * ri));
+					} else if (l instanceof IntConstant) {
+						int li = ((IntConstant) l).getValue();
+						stack.push(scale(li, r));
+					} else if (r instanceof IntConstant) {
+						int ri = ((IntConstant) r).getValue();
+						stack.push(scale(ri, l));
+					} else {
+						stack.clear();
+						linearInteger = false;
+					}
+				}
+				break;
+			case NOT:
+				if (!stack.isEmpty()) {
+					Expression e = stack.pop();
+					if (e.equals(Operation.TRUE)) {
+						e = Operation.FALSE;
+					} else if (e.equals(Operation.FALSE)) {
+						e = Operation.TRUE;
+					} else if (e instanceof Operation) {
+						Operation o = (Operation) e;
+						switch (o.getOperator()) {
+						case NOT:
+							e = o.getOperand(0);
+							break;
+						case EQ:
+							e = new Operation(Operation.Operator.NE, o.getOperand(0), o.getOperand(1));
+							break;
+						case NE:
+							e = new Operation(Operation.Operator.EQ, o.getOperand(0), o.getOperand(1));
+							break;
+						case GE:
+							e = new Operation(Operation.Operator.LT, o.getOperand(0), o.getOperand(1));
+							break;
+						case GT:
+							e = new Operation(Operation.Operator.LE, o.getOperand(0), o.getOperand(1));
+							break;
+						case LE:
+							e = new Operation(Operation.Operator.GT, o.getOperand(0), o.getOperand(1));
+							break;
+						case LT:
+							e = new Operation(Operation.Operator.GE, o.getOperand(0), o.getOperand(1));
+							break;
+						default:
+							break;
+						}
+					} else {
+						// We just drop the NOT??
+					}
+					stack.push(e);
+				} else {
+					// We just drop the NOT??
+				}
+				break;
+			default:
+				break;
+			}
+		}
+
+		private Expression merge(Expression left, Expression right) {
+			Operation l = null;
+			Operation r = null;
+			int s = 0;
+			if (left instanceof IntConstant) {
+				s = ((IntConstant) left).getValue();
+			} else {
+				if (hasRightConstant(left)) {
+					s = getRightConstant(left);
+					l = getLeftOperation(left);
+				} else {
+					l = (Operation) left;
+				}
+			}
+			if (right instanceof IntConstant) {
+				s += ((IntConstant) right).getValue();
+			} else {
+				if (hasRightConstant(right)) {
+					s += getRightConstant(right);
+					r = getLeftOperation(right);
+				} else {
+					r = (Operation) right;
+				}
+			}
+			SortedMap<Variable, Integer> coefficients = new TreeMap<Variable, Integer>();
+			IntConstant c;
+			Variable v;
+			Integer k;
+
+			// Collect the coefficients of l
+			if (l != null) {
+				while (l.getOperator() == Operation.Operator.ADD) {
+					Operation o = (Operation) l.getOperand(1);
+					assert (o.getOperator() == Operation.Operator.MUL);
+					c = (IntConstant) o.getOperand(0);
+					v = (IntVariable) o.getOperand(1);
+					coefficients.put(v, c.getValue());
+					l = (Operation) l.getOperand(0);
+				}
+				assert (l.getOperator() == Operation.Operator.MUL);
+				c = (IntConstant) l.getOperand(0);
+				v = (IntVariable) l.getOperand(1);
+				coefficients.put(v, c.getValue());
+			}
+
+			// Collect the coefficients of r
+			if (r != null) {
+				while (r.getOperator() == Operation.Operator.ADD) {
+					Operation o = (Operation) r.getOperand(1);
+					assert (o.getOperator() == Operation.Operator.MUL);
+					c = (IntConstant) o.getOperand(0);
+					v = (IntVariable) o.getOperand(1);
+					k = coefficients.get(v);
+					if (k == null) {
+						coefficients.put(v, c.getValue());
+					} else {
+						coefficients.put(v, c.getValue() + k);
+					}
+					r = (Operation) r.getOperand(0);
+				}
+				assert (r.getOperator() == Operation.Operator.MUL);
+				c = (IntConstant) r.getOperand(0);
+				v = (IntVariable) r.getOperand(1);
+				k = coefficients.get(v);
+				if (k == null) {
+					coefficients.put(v, c.getValue());
+				} else {
+					coefficients.put(v, c.getValue() + k);
+				}
+			}
+
+			Expression lr = null;
+			for (Map.Entry<Variable, Integer> e : coefficients.entrySet()) {
+				int coef = e.getValue();
+				if (coef != 0) {
+					Operation term = new Operation(Operation.Operator.MUL,
+							new IntConstant(coef), e.getKey());
+					if (lr == null) {
+						lr = term;
+					} else {
+						lr = new Operation(Operation.Operator.ADD, lr, term);
+					}
+				}
+			}
+			if ((lr == null) || (lr instanceof IntConstant)) {
+				return new IntConstant(s);
+			} else if (s == 0) {
+				return lr;
+			} else {
+				return new Operation(Operation.Operator.ADD, lr,
+						new IntConstant(s));
+			}
+		}
+
+		private boolean hasRightConstant(Expression expression) {
+			return isAddition(expression)
+					&& (getRightExpression(expression) instanceof IntConstant);
+		}
+
+		private int getRightConstant(Expression expression) {
+			return ((IntConstant) getRightExpression(expression)).getValue();
+		}
+
+		private Expression getLeftExpression(Expression expression) {
+			return ((Operation) expression).getOperand(0);
+		}
+
+		private Expression getRightExpression(Expression expression) {
+			return ((Operation) expression).getOperand(1);
+		}
+
+		private Operation getLeftOperation(Expression expression) {
+			return (Operation) getLeftExpression(expression);
+		}
+
+		private boolean isAddition(Expression expression) {
+			return ((Operation) expression).getOperator() == Operation.Operator.ADD;
+		}
+
+		private Expression scale(int factor, Expression expression) {
+			if (factor == 0) {
+				return Operation.ZERO;
+			}
+			if (expression instanceof IntConstant) {
+				return new IntConstant(factor
+						* ((IntConstant) expression).getValue());
+			} else if (expression instanceof IntVariable) {
+				return expression;
+			} else {
+				assert (expression instanceof Operation);
+				Operation o = (Operation) expression;
+				Operation.Operator p = o.getOperator();
+				Expression l = scale(factor, o.getOperand(0));
+				Expression r = scale(factor, o.getOperand(1));
+				return new Operation(p, l, r);
+			}
+		}
+
+	}
+
+	private static class Renamer extends Visitor {
+
+		private Map<Variable, Variable> map;
+
+		private Stack<Expression> stack;
+
+		public Renamer(Map<Variable, Variable> map,
+				SortedSet<IntVariable> variableSet) {
+			this.map = map;
+			stack = new Stack<Expression>();
+		}
+
+		public Expression rename(Expression expression) throws VisitorException {
+			expression.accept(this);
+			return stack.pop();
+		}
+
+		@Override
+		public void postVisit(IntVariable variable) {
+			Variable v = map.get(variable);
+			if (v == null) {
+				v = new IntVariable("v" + map.size(), variable.getLowerBound(),
+						variable.getUpperBound());
+				map.put(variable, v);
+			}
+			stack.push(v);
+		}
+
+		@Override
+		public void postVisit(IntConstant constant) {
+			stack.push(constant);
+		}
+
+		@Override
+		public void postVisit(Operation operation) {
+			int arity = operation.getOperator().getArity();
+			Expression operands[] = new Expression[arity];
+			for (int i = arity; i > 0; i--) {
+				operands[i - 1] = stack.pop();
+			}
+			stack.push(new Operation(operation.getOperator(), operands));
+		}
+
+	}
+
+}
diff --git a/test/za/ac/sun/cs/green/EntireSuite.java b/test/za/ac/sun/cs/green/EntireSuite.java
index d48bb8c9..f7ce0768 100644
--- a/test/za/ac/sun/cs/green/EntireSuite.java
+++ b/test/za/ac/sun/cs/green/EntireSuite.java
@@ -32,6 +32,7 @@
 import za.ac.sun.cs.green.util.ParallelSATTest;
 import za.ac.sun.cs.green.util.SetServiceTest;
 import za.ac.sun.cs.green.util.SetTaskManagerTest;
+import za.ac.sun.cs.green.service.simplify.OnlyConstantPropogationTest;
 
 @RunWith(Suite.class)
 @Suite.SuiteClasses({
diff --git a/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java b/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java
index 03f62ccf..7c7b9fb1 100644
--- a/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java
+++ b/test/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.java
@@ -77,7 +77,10 @@ public void test01() {
 		Operation o = new Operation(Operation.Operator.EQ, v, c);
 		check(o, "aa==0", "1*v==0");
 	}
+	/* Changed last line from "check(o3, "(aa==0)&&(bb!=1)", "1*v==0", "1*v+-1!=0");"
+ 		to check(o3, "(aa=<0)&&(bb!=1)", "1*v==0", "1*v+-1!=0");
 
+	*/
 	@Test
 	public void test02() {
 		IntVariable v1 = new IntVariable("aa", 0, 99);
@@ -100,7 +103,7 @@ public void test03() {
 		Operation o2 = new Operation(Operation.Operator.NE, v2, c2);
 		check(o1, o2, "(aa==0)&&(bb!=1)", "1*v==0");
 	}
-
+ 
 	@Test
 	public void test04() {
 		IntVariable v1 = new IntVariable("aa", 0, 99);
@@ -293,7 +296,7 @@ public void test19() {
 		Operation o1 = new Operation(Operation.Operator.LE, c1, c1);
 		check(o1, "2<=2", "0==0");
 	}
-/*
+
 	@Test
 	public void test20() {
 		IntConstant c1 = new IntConstant(2);
@@ -301,7 +304,7 @@ public void test20() {
 		Operation o1 = new Operation(Operation.Operator.LE, c1, c1);
 		Operation o2 = new Operation(Operation.Operator.LT, v1, c1);
 		Operation o3 = new Operation(Operation.Operator.AND, o1, o2);
-		check(o3, "(2<=2)&&(aa<2)", "1*v+-1<0");
+		check(o3, "(2<=2)&&(aa<2)", "1*v+-1<=0");
 	}
-*/
+
 }
diff --git a/test/za/ac/sun/cs/green/service/simplify/.OnlyConstantPropogationTest.java.swp b/test/za/ac/sun/cs/green/service/simplify/.OnlyConstantPropogationTest.java.swp
new file mode 100644
index 00000000..d15500c9
Binary files /dev/null and b/test/za/ac/sun/cs/green/service/simplify/.OnlyConstantPropogationTest.java.swp differ
diff --git a/test/za/ac/sun/cs/green/service/simplify/OnlyConstantPropogationTest.java b/test/za/ac/sun/cs/green/service/simplify/OnlyConstantPropogationTest.java
new file mode 100644
index 00000000..772d5c5c
--- /dev/null
+++ b/test/za/ac/sun/cs/green/service/simplify/OnlyConstantPropogationTest.java
@@ -0,0 +1,75 @@
+package za.ac.sun.cs.green.service.simplify;
+
+import static org.junit.Assert.*;
+
+import java.util.Arrays;
+import java.util.Properties;
+import java.util.SortedSet;
+import java.util.TreeSet;
+
+import org.junit.BeforeClass;
+import org.junit.Test;
+
+import za.ac.sun.cs.green.Instance;
+import za.ac.sun.cs.green.Green;
+import za.ac.sun.cs.green.expr.Expression;
+import za.ac.sun.cs.green.expr.IntConstant;
+import za.ac.sun.cs.green.expr.IntVariable;
+import za.ac.sun.cs.green.expr.Operation;
+import za.ac.sun.cs.green.util.Configuration;
+
+public class OnlyConstantPropogationTest {
+
+	public static Green solver;
+
+	@BeforeClass
+		public static void initialize() {
+			solver = new Green();
+			System.out.println("hello llaow");
+			Properties props = new Properties();
+			props.setProperty("green.services", "sat");
+			props.setProperty("green.service.sat", "(simplify sink)");
+			//props.setProperty("green.service.sat", "(canonize sink)");
+			props.setProperty("green.service.sat.simplify",
+					"za.ac.sun.cs.green.service.simplify.ConstantPropogation");
+			//props.setProperty("green.service.sat.canonize",
+			//		"za.ac.sun.cs.green.service.canonizer.SATCanonizerService");
+			
+			props.setProperty("green.service.sat.sink",
+					"za.ac.sun.cs.green.service.sink.SinkService");
+			Configuration config = new Configuration(solver, props);
+			config.configure();
+		}
+
+	private void finalCheck(String observed, String expected) {
+		assertEquals(expected, observed);
+	}
+
+	private void check(Expression expression, String expected) {
+		Instance i = new Instance(solver, null, null, expression);
+		Expression e = i.getExpression();
+		assertTrue(e.equals(expression));
+		assertEquals(expression.toString(), e.toString());
+		Object result = i.request("sat");
+		assertNotNull(result);
+		assertEquals(Instance.class, result.getClass());
+		Instance j = (Instance) result;
+		finalCheck(j.getExpression().toString(), expected);
+	}
+
+	@Test
+	public void test00() {
+		IntVariable x = new IntVariable("x", 0, 99);
+		IntVariable y = new IntVariable("y", 0, 99);
+		IntVariable z = new IntVariable("z", 0, 99);
+		IntConstant c = new IntConstant(1);
+		IntConstant c10 = new IntConstant(10);
+		IntConstant c3 = new IntConstant(3);
+		Operation o1 = new Operation(Operation.Operator.EQ, x, c); // o1 : x = 1
+		Operation o2 = new Operation(Operation.Operator.ADD, x, y); // o2 : (x + y)
+		Operation o3 = new Operation(Operation.Operator.EQ, o2, c10); // o3 : x+y = 10
+		Operation o4 = new Operation(Operation.Operator.AND, o1, o3); // o4 : x = 1 && (x+y) = 10 
+		check(o4, "(x==1)&&((1+y)==10)");
+	}
+
+}
diff --git a/test/za/ac/sun/cs/green/service/simplify/SimplificationConstantPropogationTest.java b/test/za/ac/sun/cs/green/service/simplify/SimplificationConstantPropogationTest.java
new file mode 100644
index 00000000..c7995ac6
--- /dev/null
+++ b/test/za/ac/sun/cs/green/service/simplify/SimplificationConstantPropogationTest.java
@@ -0,0 +1,186 @@
+package za.ac.sun.cs.green.service.simplify;
+
+import static org.junit.Assert.*;
+
+import java.util.Arrays;
+import java.util.Properties;
+import java.util.SortedSet;
+import java.util.TreeSet;
+
+import org.junit.BeforeClass;
+import org.junit.Test;
+
+import za.ac.sun.cs.green.Instance;
+import za.ac.sun.cs.green.Green;
+import za.ac.sun.cs.green.expr.Expression;
+import za.ac.sun.cs.green.expr.IntConstant;
+import za.ac.sun.cs.green.expr.IntVariable;
+import za.ac.sun.cs.green.expr.Operation;
+import za.ac.sun.cs.green.util.Configuration;
+
+public class SimplificationConstantPropogationTest {
+
+	public static Green solver;
+
+	@BeforeClass
+		public static void initialize() {
+			solver = new Green();
+			Properties props = new Properties();
+			props.setProperty("green.services", "sat");
+			props.setProperty("green.service.sat", "(simplify sink)");
+			//props.setProperty("green.service.sat", "(canonize sink)");
+			props.setProperty("green.service.sat.simplify",
+					"za.ac.sun.cs.green.service.simplify.ConstantPropogation");
+			//props.setProperty("green.service.sat.canonize",
+			//		"za.ac.sun.cs.green.service.canonizer.SATCanonizerService");
+			
+			props.setProperty("green.service.sat.sink",
+					"za.ac.sun.cs.green.service.sink.SinkService");
+			Configuration config = new Configuration(solver, props);
+			config.configure();
+		}
+
+	private void finalCheck(String observed, String expected) {
+		assertEquals(expected, observed);
+	}
+
+	private void check(Expression expression, String expected) {
+		Instance i = new Instance(solver, null, null, expression);
+		Expression e = i.getExpression();
+		assertTrue(e.equals(expression));
+		assertEquals(expression.toString(), e.toString());
+		Object result = i.request("sat");
+		assertNotNull(result);
+		assertEquals(Instance.class, result.getClass());
+		Instance j = (Instance) result;
+		finalCheck(j.getExpression().toString(), expected);
+	}
+
+	@Test
+	public void test00() {
+		IntVariable x = new IntVariable("x", 0, 99);
+		IntVariable y = new IntVariable("y", 0, 99);
+		IntVariable z = new IntVariable("z", 0, 99);
+		IntConstant c = new IntConstant(1);
+		IntConstant c10 = new IntConstant(10);
+		IntConstant c3 = new IntConstant(3);
+		Operation o1 = new Operation(Operation.Operator.EQ, x, c); // o1 : x = 1
+		Operation o2 = new Operation(Operation.Operator.ADD, x, y); // o2 : (x + y)
+		Operation o3 = new Operation(Operation.Operator.EQ, o2, c10); // o3 : x+y = 10
+		Operation o4 = new Operation(Operation.Operator.AND, o1, o3); // o4 : x = 1 && (x+y) = 10 
+		check(o4, "(x==1)&&(y==9)");
+	}
+	
+	@Test
+	public void test01() {
+		IntVariable x = new IntVariable("x", 0, 99);
+		IntVariable y = new IntVariable("y", 0, 99);
+		IntConstant c = new IntConstant(1);
+		IntConstant c2 = new IntConstant(10);
+		IntConstant c3 = new IntConstant(2);
+		Operation o1 = new Operation(Operation.Operator.EQ, x, c); // o1 : (x = 1)
+		Operation o2 = new Operation(Operation.Operator.ADD, x, y); // o2 : x + y
+		Operation o3 = new Operation(Operation.Operator.LT, o2, c2); // o3 : (x+y) < 10
+		Operation oi = new Operation(Operation.Operator.SUB, y, c); // oi : y-1
+		Operation o4 = new Operation(Operation.Operator.EQ, oi, c3); // o4 : y-1 = 2
+		Operation o5 = new Operation(Operation.Operator.AND, o1, o3); // o5 : (x = 1) && (x+y < 10)
+		Operation o = new Operation(Operation.Operator.AND, o5, o4); // o = (x = 1) && (x+y < 10) && (y-1 = 2)
+		// (x = 1) && (x+y < 10) && (y-1 = 2)
+		check(o, "(x==1)&&(y==3)");
+	}
+
+	@Test
+		public void test02() {
+			IntConstant c1 = new IntConstant(4);
+			IntConstant c2 = new IntConstant(10);
+			Operation o = new Operation(Operation.Operator.LT, c1, c2);
+			check(o, "0==0");
+		}
+
+	@Test
+		public void test03() {
+			IntConstant c1 = new IntConstant(4);
+			IntConstant c2 = new IntConstant(10);
+			Operation o = new Operation(Operation.Operator.GT, c1, c2);
+			check(o, "0==1");
+		}
+
+	@Test
+		public void test04() {
+			IntConstant c1 = new IntConstant(4);
+			IntConstant c2 = new IntConstant(10);
+			Operation o1 = new Operation(Operation.Operator.LT, c1, c2);
+			Operation o2 = new Operation(Operation.Operator.GT, c1, c2);
+			Operation o = new Operation(Operation.Operator.AND, o1, o2);
+			check(o, "0==1");
+		}
+
+
+
+
+	@Test
+		public void test05() {
+			IntVariable x = new IntVariable("x", 0, 99);
+			IntVariable y = new IntVariable("y", 0, 99);		
+			IntConstant c = new IntConstant(1);
+			IntConstant c2 = new IntConstant(10);
+			IntConstant c3 = new IntConstant(2);
+			Operation o1 = new Operation(Operation.Operator.EQ, c, x);
+			Operation o2 = new Operation(Operation.Operator.ADD, x, y);
+			Operation o3 = new Operation(Operation.Operator.LT, o2, c2);
+			Operation oi = new Operation(Operation.Operator.SUB, y, c);		
+			Operation o4 = new Operation(Operation.Operator.EQ, c3, oi);
+			Operation o5 = new Operation(Operation.Operator.AND, o1, o3);
+			Operation o = new Operation(Operation.Operator.AND, o5, o4);
+			check(o, "(1==x)&&(3==y)");
+		}
+
+	@Test
+		public void test06() {
+			IntVariable x = new IntVariable("x", 0, 99);
+			IntVariable y = new IntVariable("y", 0, 99);
+			IntVariable z = new IntVariable("z", 0 , 99);
+			IntConstant c = new IntConstant(1);
+			Operation o1 = new Operation(Operation.Operator.EQ, x, y);		
+			Operation o2 = new Operation(Operation.Operator.EQ, y, z);
+			Operation o3 = new Operation(Operation.Operator.EQ, z, c);
+			Operation o = new Operation(Operation.Operator.AND, o1, o2);
+			o = new Operation(Operation.Operator.AND, o, o3);
+			check(o, "(x==1)&&((y==1)&&(z==1))");
+		}
+
+	@Test
+		public void test07() {
+			IntVariable x = new IntVariable("x", 0, 99);
+			IntVariable y = new IntVariable("y", 0, 99);
+			IntVariable z = new IntVariable("z", 0 , 99);
+			IntConstant c = new IntConstant(2);
+			IntConstant c1 = new IntConstant(4);
+			Operation o1 = new Operation(Operation.Operator.MUL, x, y);		
+			Operation o2 = new Operation(Operation.Operator.EQ, z, o1); // z = x * y
+			Operation o3 = new Operation(Operation.Operator.EQ, x, c); // x = 2
+			Operation o4 = new Operation(Operation.Operator.ADD, y, x); 
+			Operation o5 = new Operation(Operation.Operator.EQ, o4, c1); // x+y = 4
+
+			Operation o = new Operation(Operation.Operator.AND, o2, o3); // z = x * y && x = 2
+			o = new Operation(Operation.Operator.AND, o, o5); // z = x * y && x = 2 && x+y = 4
+			check(o, "(z==4)&&((x==2)&&(y==2))");
+		}
+
+	@Test
+		public void test08() {
+			IntVariable x = new IntVariable("x", 0, 99);
+			IntConstant c = new IntConstant(2);
+			IntConstant c1 = new IntConstant(4);
+			Operation o1 = new Operation(Operation.Operator.EQ, x, c);		
+			Operation o2 = new Operation(Operation.Operator.EQ, x, c1);
+			Operation o = new Operation(Operation.Operator.AND, o1, o2);
+			
+			check(o, "0==1");
+		}
+
+
+
+
+
+}