diff --git a/.travis.yml b/.travis.yml
index 4651be32..c1f1822a 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -1,5 +1,13 @@
+sudo: required
+
language: java
+services:
+ - docker
+
+before_install:
+ - docker build -t francois .
+
script:
- - ant;
- - ant test;
+ - docker run francois sh -c "ant; ant test;"
+
diff --git a/Dockerfile b/Dockerfile
index e465a44f..2a01b7ae 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/FrancoisVGit/green
# Download and extract Z3
RUN mkdir z3
diff --git a/README.md b/README.md
index aedc3ddc..1a2096fe 100644
--- a/README.md
+++ b/README.md
@@ -1,4 +1,5 @@
-[![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/FrancoisVGit/green.svg?branch=master)](https://travis-ci.org/FrancoisVGit/green?branch=master)
Notes:
diff --git a/bin/build.properties b/bin/build.properties
new file mode 100644
index 00000000..87eee8da
--- /dev/null
+++ b/bin/build.properties
@@ -0,0 +1,17 @@
+# Build properties for green.
+#
+# It is OK to to change these properties if they do not agree with your
+# setup, but do not commit it to the repository.
+
+#target = 1.7
+#source = 1.7
+#bootpath = /Library/Java/JavaVirtualMachines/jdk1.7.0_75.jdk/Contents/Home/jre/lib/rt.jar
+
+target = 1.8
+source = 1.8
+bootpath = /Library/Java/JavaVirtualMachines/jdk1.8.0_45.jdk/Contents/Home/jre/lib/rt.jar
+
+cvc3lib = /Users/jaco/Documents/RESEARCH/SYMEXE/cvc3-2.4.1/java/lib
+lattepath = /Users/jaco/Documents/RESEARCH/latte-integrale-1.7.3/latte-int-1.7.3/code/latte/count
+z3path = /Users/jaco/Documents/RESEARCH/SYMEXE/Z3/build/z3
+z3lib = ${basedir}/lib
diff --git a/bin/junit/TESTS-TestSuites.xml b/bin/junit/TESTS-TestSuites.xml
new file mode 100644
index 00000000..511be84d
--- /dev/null
+++ b/bin/junit/TESTS-TestSuites.xml
@@ -0,0 +1,2 @@
+
+
diff --git a/bin/junit/all-tests.html b/bin/junit/all-tests.html
new file mode 100644
index 00000000..c3de1b0c
--- /dev/null
+++ b/bin/junit/all-tests.html
@@ -0,0 +1,22 @@
+
+
+
+Unit Test Results: All Tests
+
+
+
+Unit Test Results.
+
+
+ | Designed for use with JUnit and Ant. |
+
+
+
+All Tests
+
+
+Class | Name | Status | Type | Time(s) |
+
+
+
+
diff --git a/bin/junit/allclasses-frame.html b/bin/junit/allclasses-frame.html
new file mode 100644
index 00000000..674585a9
--- /dev/null
+++ b/bin/junit/allclasses-frame.html
@@ -0,0 +1,11 @@
+
+
+
+All Unit Test Classes
+
+
+
+Classes
+
+
+
diff --git a/bin/junit/alltests-errors.html b/bin/junit/alltests-errors.html
new file mode 100644
index 00000000..deb82916
--- /dev/null
+++ b/bin/junit/alltests-errors.html
@@ -0,0 +1,22 @@
+
+
+
+Unit Test Results: All Errors
+
+
+
+Unit Test Results.
+
+
+ | Designed for use with JUnit and Ant. |
+
+
+
+All Errors
+
+
+Class | Name | Status | Type | Time(s) |
+
+
+
+
diff --git a/bin/junit/alltests-fails.html b/bin/junit/alltests-fails.html
new file mode 100644
index 00000000..a762062c
--- /dev/null
+++ b/bin/junit/alltests-fails.html
@@ -0,0 +1,22 @@
+
+
+
+Unit Test Results: All Failures
+
+
+
+Unit Test Results.
+
+
+ | Designed for use with JUnit and Ant. |
+
+
+
+All Failures
+
+
+Class | Name | Status | Type | Time(s) |
+
+
+
+
diff --git a/bin/junit/alltests-skipped.html b/bin/junit/alltests-skipped.html
new file mode 100644
index 00000000..a08afc5b
--- /dev/null
+++ b/bin/junit/alltests-skipped.html
@@ -0,0 +1,22 @@
+
+
+
+Unit Test Results: All Skipped
+
+
+
+Unit Test Results.
+
+
+ | Designed for use with JUnit and Ant. |
+
+
+
+All Skipped
+
+
+Class | Name | Status | Type | Time(s) |
+
+
+
+
diff --git a/bin/junit/index.html b/bin/junit/index.html
new file mode 100644
index 00000000..4163d4e8
--- /dev/null
+++ b/bin/junit/index.html
@@ -0,0 +1,19 @@
+
+
+
+Unit Test Results.
+
+
+
diff --git a/bin/junit/overview-frame.html b/bin/junit/overview-frame.html
new file mode 100644
index 00000000..948bdc67
--- /dev/null
+++ b/bin/junit/overview-frame.html
@@ -0,0 +1,14 @@
+
+
+
+All Unit Test Packages
+
+
+
+
+Packages
+
+
+
diff --git a/bin/junit/overview-summary.html b/bin/junit/overview-summary.html
new file mode 100644
index 00000000..d469d002
--- /dev/null
+++ b/bin/junit/overview-summary.html
@@ -0,0 +1,38 @@
+
+
+
+Unit Test Results: Summary
+
+
+
+Unit Test Results.
+
+
+ | Designed for use with JUnit and Ant. |
+
+
+
+Summary
+
+
+Tests | Failures | Errors | Skipped | Success rate | Time |
+
+
+0 | 0 | 0 | 0 | NaN | 0.000 |
+
+
+
+
+
+ Note: failures are anticipated and checked for with assertions while errors are unanticipated.
+ |
+
+
+Packages
+
+
+Name | Tests | Errors | Failures | Skipped | Time(s) | Time Stamp | Host |
+
+
+
+
diff --git a/bin/junit/stylesheet.css b/bin/junit/stylesheet.css
new file mode 100644
index 00000000..c371da68
--- /dev/null
+++ b/bin/junit/stylesheet.css
@@ -0,0 +1,48 @@
+
+body {
+ font:normal 68% verdana,arial,helvetica;
+ color:#000000;
+}
+table tr td, table tr th {
+ font-size: 68%;
+}
+table.details tr th{
+ font-weight: bold;
+ text-align:left;
+ background:#a6caf0;
+}
+table.details tr td{
+ background:#eeeee0;
+}
+
+p {
+ line-height:1.5em;
+ margin-top:0.5em; margin-bottom:1.0em;
+}
+h1 {
+ margin: 0px 0px 5px; font: 165% verdana,arial,helvetica
+}
+h2 {
+ margin-top: 1em; margin-bottom: 0.5em; font: bold 125% verdana,arial,helvetica
+}
+h3 {
+ margin-bottom: 0.5em; font: bold 115% verdana,arial,helvetica
+}
+h4 {
+ margin-bottom: 0.5em; font: bold 100% verdana,arial,helvetica
+}
+h5 {
+ margin-bottom: 0.5em; font: bold 100% verdana,arial,helvetica
+}
+h6 {
+ margin-bottom: 0.5em; font: bold 100% verdana,arial,helvetica
+}
+.Error {
+ font-weight:bold; color:red;
+}
+.Failure {
+ font-weight:bold; color:purple;
+}
+.Properties {
+ text-align:right;
+}
diff --git a/bin/za/ac/sun/cs/green/EntireSuite.class b/bin/za/ac/sun/cs/green/EntireSuite.class
new file mode 100644
index 00000000..9e659314
Binary files /dev/null and b/bin/za/ac/sun/cs/green/EntireSuite.class differ
diff --git a/bin/za/ac/sun/cs/green/Green$1.class b/bin/za/ac/sun/cs/green/Green$1.class
new file mode 100644
index 00000000..2145545c
Binary files /dev/null and b/bin/za/ac/sun/cs/green/Green$1.class differ
diff --git a/bin/za/ac/sun/cs/green/Green.class b/bin/za/ac/sun/cs/green/Green.class
new file mode 100644
index 00000000..252de682
Binary files /dev/null and b/bin/za/ac/sun/cs/green/Green.class differ
diff --git a/bin/za/ac/sun/cs/green/Instance.class b/bin/za/ac/sun/cs/green/Instance.class
new file mode 100644
index 00000000..006c8285
Binary files /dev/null and b/bin/za/ac/sun/cs/green/Instance.class differ
diff --git a/bin/za/ac/sun/cs/green/Service.class b/bin/za/ac/sun/cs/green/Service.class
new file mode 100644
index 00000000..56f1db9f
Binary files /dev/null and b/bin/za/ac/sun/cs/green/Service.class differ
diff --git a/bin/za/ac/sun/cs/green/expr/Constant.class b/bin/za/ac/sun/cs/green/expr/Constant.class
new file mode 100644
index 00000000..5bc4dfb7
Binary files /dev/null and b/bin/za/ac/sun/cs/green/expr/Constant.class differ
diff --git a/bin/za/ac/sun/cs/green/expr/Expression.class b/bin/za/ac/sun/cs/green/expr/Expression.class
new file mode 100644
index 00000000..2294d019
Binary files /dev/null and b/bin/za/ac/sun/cs/green/expr/Expression.class differ
diff --git a/bin/za/ac/sun/cs/green/expr/IntConstant.class b/bin/za/ac/sun/cs/green/expr/IntConstant.class
new file mode 100644
index 00000000..e512727a
Binary files /dev/null and b/bin/za/ac/sun/cs/green/expr/IntConstant.class differ
diff --git a/bin/za/ac/sun/cs/green/expr/IntVariable.class b/bin/za/ac/sun/cs/green/expr/IntVariable.class
new file mode 100644
index 00000000..70359164
Binary files /dev/null and b/bin/za/ac/sun/cs/green/expr/IntVariable.class differ
diff --git a/bin/za/ac/sun/cs/green/expr/Operation$1$1.class b/bin/za/ac/sun/cs/green/expr/Operation$1$1.class
new file mode 100644
index 00000000..afb34d2a
Binary files /dev/null and b/bin/za/ac/sun/cs/green/expr/Operation$1$1.class differ
diff --git a/bin/za/ac/sun/cs/green/expr/Operation$1.class b/bin/za/ac/sun/cs/green/expr/Operation$1.class
new file mode 100644
index 00000000..2624d179
Binary files /dev/null and b/bin/za/ac/sun/cs/green/expr/Operation$1.class differ
diff --git a/bin/za/ac/sun/cs/green/expr/Operation$2.class b/bin/za/ac/sun/cs/green/expr/Operation$2.class
new file mode 100644
index 00000000..bca1341f
Binary files /dev/null and b/bin/za/ac/sun/cs/green/expr/Operation$2.class differ
diff --git a/bin/za/ac/sun/cs/green/expr/Operation$Fix.class b/bin/za/ac/sun/cs/green/expr/Operation$Fix.class
new file mode 100644
index 00000000..88aa6bce
Binary files /dev/null and b/bin/za/ac/sun/cs/green/expr/Operation$Fix.class differ
diff --git a/bin/za/ac/sun/cs/green/expr/Operation$Operator.class b/bin/za/ac/sun/cs/green/expr/Operation$Operator.class
new file mode 100644
index 00000000..c339ef48
Binary files /dev/null and b/bin/za/ac/sun/cs/green/expr/Operation$Operator.class differ
diff --git a/bin/za/ac/sun/cs/green/expr/Operation.class b/bin/za/ac/sun/cs/green/expr/Operation.class
new file mode 100644
index 00000000..f50f83a2
Binary files /dev/null and b/bin/za/ac/sun/cs/green/expr/Operation.class differ
diff --git a/bin/za/ac/sun/cs/green/expr/RealConstant.class b/bin/za/ac/sun/cs/green/expr/RealConstant.class
new file mode 100644
index 00000000..f1e54c54
Binary files /dev/null and b/bin/za/ac/sun/cs/green/expr/RealConstant.class differ
diff --git a/bin/za/ac/sun/cs/green/expr/RealVariable.class b/bin/za/ac/sun/cs/green/expr/RealVariable.class
new file mode 100644
index 00000000..adc2e79d
Binary files /dev/null and b/bin/za/ac/sun/cs/green/expr/RealVariable.class differ
diff --git a/bin/za/ac/sun/cs/green/expr/StringConstant.class b/bin/za/ac/sun/cs/green/expr/StringConstant.class
new file mode 100644
index 00000000..02a7563a
Binary files /dev/null and b/bin/za/ac/sun/cs/green/expr/StringConstant.class differ
diff --git a/bin/za/ac/sun/cs/green/expr/StringVariable.class b/bin/za/ac/sun/cs/green/expr/StringVariable.class
new file mode 100644
index 00000000..75b1a9ed
Binary files /dev/null and b/bin/za/ac/sun/cs/green/expr/StringVariable.class differ
diff --git a/bin/za/ac/sun/cs/green/expr/Variable.class b/bin/za/ac/sun/cs/green/expr/Variable.class
new file mode 100644
index 00000000..133823b0
Binary files /dev/null and b/bin/za/ac/sun/cs/green/expr/Variable.class differ
diff --git a/bin/za/ac/sun/cs/green/expr/Visitor.class b/bin/za/ac/sun/cs/green/expr/Visitor.class
new file mode 100644
index 00000000..9b47d334
Binary files /dev/null and b/bin/za/ac/sun/cs/green/expr/Visitor.class differ
diff --git a/bin/za/ac/sun/cs/green/expr/VisitorException.class b/bin/za/ac/sun/cs/green/expr/VisitorException.class
new file mode 100644
index 00000000..edeed1b4
Binary files /dev/null and b/bin/za/ac/sun/cs/green/expr/VisitorException.class differ
diff --git a/bin/za/ac/sun/cs/green/log/GreenFormatter.class b/bin/za/ac/sun/cs/green/log/GreenFormatter.class
new file mode 100644
index 00000000..1765c2ba
Binary files /dev/null and b/bin/za/ac/sun/cs/green/log/GreenFormatter.class differ
diff --git a/bin/za/ac/sun/cs/green/log/GreenHandler.class b/bin/za/ac/sun/cs/green/log/GreenHandler.class
new file mode 100644
index 00000000..521cf56d
Binary files /dev/null and b/bin/za/ac/sun/cs/green/log/GreenHandler.class differ
diff --git a/bin/za/ac/sun/cs/green/misc/FactorizerCNFTest.class b/bin/za/ac/sun/cs/green/misc/FactorizerCNFTest.class
new file mode 100644
index 00000000..c40952bf
Binary files /dev/null and b/bin/za/ac/sun/cs/green/misc/FactorizerCNFTest.class differ
diff --git a/bin/za/ac/sun/cs/green/misc/SATZ3JavaCNFTest.class b/bin/za/ac/sun/cs/green/misc/SATZ3JavaCNFTest.class
new file mode 100644
index 00000000..c3805630
Binary files /dev/null and b/bin/za/ac/sun/cs/green/misc/SATZ3JavaCNFTest.class differ
diff --git a/bin/za/ac/sun/cs/green/parser/klee/ParseException.class b/bin/za/ac/sun/cs/green/parser/klee/ParseException.class
new file mode 100644
index 00000000..a6744862
Binary files /dev/null and b/bin/za/ac/sun/cs/green/parser/klee/ParseException.class differ
diff --git a/bin/za/ac/sun/cs/green/parser/klee/Parser$1.class b/bin/za/ac/sun/cs/green/parser/klee/Parser$1.class
new file mode 100644
index 00000000..16fb52b3
Binary files /dev/null and b/bin/za/ac/sun/cs/green/parser/klee/Parser$1.class differ
diff --git a/bin/za/ac/sun/cs/green/parser/klee/Parser$KArray.class b/bin/za/ac/sun/cs/green/parser/klee/Parser$KArray.class
new file mode 100644
index 00000000..c86466d5
Binary files /dev/null and b/bin/za/ac/sun/cs/green/parser/klee/Parser$KArray.class differ
diff --git a/bin/za/ac/sun/cs/green/parser/klee/Parser$KArrayVersion.class b/bin/za/ac/sun/cs/green/parser/klee/Parser$KArrayVersion.class
new file mode 100644
index 00000000..d5172651
Binary files /dev/null and b/bin/za/ac/sun/cs/green/parser/klee/Parser$KArrayVersion.class differ
diff --git a/bin/za/ac/sun/cs/green/parser/klee/Parser$KConcreteArray.class b/bin/za/ac/sun/cs/green/parser/klee/Parser$KConcreteArray.class
new file mode 100644
index 00000000..d66e2357
Binary files /dev/null and b/bin/za/ac/sun/cs/green/parser/klee/Parser$KConcreteArray.class differ
diff --git a/bin/za/ac/sun/cs/green/parser/klee/Parser$KExpression.class b/bin/za/ac/sun/cs/green/parser/klee/Parser$KExpression.class
new file mode 100644
index 00000000..5a763f36
Binary files /dev/null and b/bin/za/ac/sun/cs/green/parser/klee/Parser$KExpression.class differ
diff --git a/bin/za/ac/sun/cs/green/parser/klee/Parser$KNumber.class b/bin/za/ac/sun/cs/green/parser/klee/Parser$KNumber.class
new file mode 100644
index 00000000..04072af4
Binary files /dev/null and b/bin/za/ac/sun/cs/green/parser/klee/Parser$KNumber.class differ
diff --git a/bin/za/ac/sun/cs/green/parser/klee/Parser$KOperation.class b/bin/za/ac/sun/cs/green/parser/klee/Parser$KOperation.class
new file mode 100644
index 00000000..d70f7107
Binary files /dev/null and b/bin/za/ac/sun/cs/green/parser/klee/Parser$KOperation.class differ
diff --git a/bin/za/ac/sun/cs/green/parser/klee/Parser$KQuery$1$1.class b/bin/za/ac/sun/cs/green/parser/klee/Parser$KQuery$1$1.class
new file mode 100644
index 00000000..81e91827
Binary files /dev/null and b/bin/za/ac/sun/cs/green/parser/klee/Parser$KQuery$1$1.class differ
diff --git a/bin/za/ac/sun/cs/green/parser/klee/Parser$KQuery$1.class b/bin/za/ac/sun/cs/green/parser/klee/Parser$KQuery$1.class
new file mode 100644
index 00000000..539a64db
Binary files /dev/null and b/bin/za/ac/sun/cs/green/parser/klee/Parser$KQuery$1.class differ
diff --git a/bin/za/ac/sun/cs/green/parser/klee/Parser$KQuery.class b/bin/za/ac/sun/cs/green/parser/klee/Parser$KQuery.class
new file mode 100644
index 00000000..5e78bc66
Binary files /dev/null and b/bin/za/ac/sun/cs/green/parser/klee/Parser$KQuery.class differ
diff --git a/bin/za/ac/sun/cs/green/parser/klee/Parser$KSymbolicArray.class b/bin/za/ac/sun/cs/green/parser/klee/Parser$KSymbolicArray.class
new file mode 100644
index 00000000..a21afa9c
Binary files /dev/null and b/bin/za/ac/sun/cs/green/parser/klee/Parser$KSymbolicArray.class differ
diff --git a/bin/za/ac/sun/cs/green/parser/klee/Parser$KUpdateVersion.class b/bin/za/ac/sun/cs/green/parser/klee/Parser$KUpdateVersion.class
new file mode 100644
index 00000000..a99d9bdf
Binary files /dev/null and b/bin/za/ac/sun/cs/green/parser/klee/Parser$KUpdateVersion.class differ
diff --git a/bin/za/ac/sun/cs/green/parser/klee/Parser$KVersion.class b/bin/za/ac/sun/cs/green/parser/klee/Parser$KVersion.class
new file mode 100644
index 00000000..8bef0395
Binary files /dev/null and b/bin/za/ac/sun/cs/green/parser/klee/Parser$KVersion.class differ
diff --git a/bin/za/ac/sun/cs/green/parser/klee/Parser.class b/bin/za/ac/sun/cs/green/parser/klee/Parser.class
new file mode 100644
index 00000000..8812c5b1
Binary files /dev/null and b/bin/za/ac/sun/cs/green/parser/klee/Parser.class differ
diff --git a/bin/za/ac/sun/cs/green/parser/klee/Scanner.class b/bin/za/ac/sun/cs/green/parser/klee/Scanner.class
new file mode 100644
index 00000000..72db82f6
Binary files /dev/null and b/bin/za/ac/sun/cs/green/parser/klee/Scanner.class differ
diff --git a/bin/za/ac/sun/cs/green/parser/klee/Token.class b/bin/za/ac/sun/cs/green/parser/klee/Token.class
new file mode 100644
index 00000000..f0d0af73
Binary files /dev/null and b/bin/za/ac/sun/cs/green/parser/klee/Token.class differ
diff --git a/bin/za/ac/sun/cs/green/parser/smtlib2/Keyword0.class b/bin/za/ac/sun/cs/green/parser/smtlib2/Keyword0.class
new file mode 100644
index 00000000..ae33af97
Binary files /dev/null and b/bin/za/ac/sun/cs/green/parser/smtlib2/Keyword0.class differ
diff --git a/bin/za/ac/sun/cs/green/parser/smtlib2/ParseException.class b/bin/za/ac/sun/cs/green/parser/smtlib2/ParseException.class
new file mode 100644
index 00000000..d5b35291
Binary files /dev/null and b/bin/za/ac/sun/cs/green/parser/smtlib2/ParseException.class differ
diff --git a/bin/za/ac/sun/cs/green/parser/smtlib2/Parser0.class b/bin/za/ac/sun/cs/green/parser/smtlib2/Parser0.class
new file mode 100644
index 00000000..ce18c2cd
Binary files /dev/null and b/bin/za/ac/sun/cs/green/parser/smtlib2/Parser0.class differ
diff --git a/bin/za/ac/sun/cs/green/parser/smtlib2/SMTLIB2Parser0Test.class b/bin/za/ac/sun/cs/green/parser/smtlib2/SMTLIB2Parser0Test.class
new file mode 100644
index 00000000..2749d747
Binary files /dev/null and b/bin/za/ac/sun/cs/green/parser/smtlib2/SMTLIB2Parser0Test.class differ
diff --git a/bin/za/ac/sun/cs/green/parser/smtlib2/SMTLIB2Scanner0Test.class b/bin/za/ac/sun/cs/green/parser/smtlib2/SMTLIB2Scanner0Test.class
new file mode 100644
index 00000000..5e10f366
Binary files /dev/null and b/bin/za/ac/sun/cs/green/parser/smtlib2/SMTLIB2Scanner0Test.class differ
diff --git a/bin/za/ac/sun/cs/green/parser/smtlib2/Scanner0.class b/bin/za/ac/sun/cs/green/parser/smtlib2/Scanner0.class
new file mode 100644
index 00000000..d33a01d6
Binary files /dev/null and b/bin/za/ac/sun/cs/green/parser/smtlib2/Scanner0.class differ
diff --git a/bin/za/ac/sun/cs/green/parser/smtlib2/Token0.class b/bin/za/ac/sun/cs/green/parser/smtlib2/Token0.class
new file mode 100644
index 00000000..ce2992ae
Binary files /dev/null and b/bin/za/ac/sun/cs/green/parser/smtlib2/Token0.class differ
diff --git a/bin/za/ac/sun/cs/green/service/BasicService.class b/bin/za/ac/sun/cs/green/service/BasicService.class
new file mode 100644
index 00000000..938d73b4
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/BasicService.class differ
diff --git a/bin/za/ac/sun/cs/green/service/CountService.class b/bin/za/ac/sun/cs/green/service/CountService.class
new file mode 100644
index 00000000..4ec2024e
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/CountService.class differ
diff --git a/bin/za/ac/sun/cs/green/service/ModelService.class b/bin/za/ac/sun/cs/green/service/ModelService.class
new file mode 100644
index 00000000..a2603c70
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/ModelService.class differ
diff --git a/bin/za/ac/sun/cs/green/service/SATService.class b/bin/za/ac/sun/cs/green/service/SATService.class
new file mode 100644
index 00000000..a2820a83
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/SATService.class differ
diff --git a/bin/za/ac/sun/cs/green/service/barvinok/CountBarvinokService$HMatrix$1.class b/bin/za/ac/sun/cs/green/service/barvinok/CountBarvinokService$HMatrix$1.class
new file mode 100644
index 00000000..52a33432
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/barvinok/CountBarvinokService$HMatrix$1.class differ
diff --git a/bin/za/ac/sun/cs/green/service/barvinok/CountBarvinokService$HMatrix.class b/bin/za/ac/sun/cs/green/service/barvinok/CountBarvinokService$HMatrix.class
new file mode 100644
index 00000000..ae232ebb
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/barvinok/CountBarvinokService$HMatrix.class differ
diff --git a/bin/za/ac/sun/cs/green/service/barvinok/CountBarvinokService$HRow.class b/bin/za/ac/sun/cs/green/service/barvinok/CountBarvinokService$HRow.class
new file mode 100644
index 00000000..558cc276
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/barvinok/CountBarvinokService$HRow.class differ
diff --git a/bin/za/ac/sun/cs/green/service/barvinok/CountBarvinokService$Subsetter.class b/bin/za/ac/sun/cs/green/service/barvinok/CountBarvinokService$Subsetter.class
new file mode 100644
index 00000000..e83e6331
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/barvinok/CountBarvinokService$Subsetter.class differ
diff --git a/bin/za/ac/sun/cs/green/service/barvinok/CountBarvinokService.class b/bin/za/ac/sun/cs/green/service/barvinok/CountBarvinokService.class
new file mode 100644
index 00000000..89ab545b
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/barvinok/CountBarvinokService.class differ
diff --git a/bin/za/ac/sun/cs/green/service/barvinok/CountBarvinokTest.class b/bin/za/ac/sun/cs/green/service/barvinok/CountBarvinokTest.class
new file mode 100644
index 00000000..491ee8d6
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/barvinok/CountBarvinokTest.class differ
diff --git a/bin/za/ac/sun/cs/green/service/barvinok/CountBarvinokWithBounderTest.class b/bin/za/ac/sun/cs/green/service/barvinok/CountBarvinokWithBounderTest.class
new file mode 100644
index 00000000..470cf4d9
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/barvinok/CountBarvinokWithBounderTest.class differ
diff --git a/bin/za/ac/sun/cs/green/service/bounder/BounderService$VariableCollector.class b/bin/za/ac/sun/cs/green/service/bounder/BounderService$VariableCollector.class
new file mode 100644
index 00000000..b2a2fe95
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/bounder/BounderService$VariableCollector.class differ
diff --git a/bin/za/ac/sun/cs/green/service/bounder/BounderService.class b/bin/za/ac/sun/cs/green/service/bounder/BounderService.class
new file mode 100644
index 00000000..866f7d4f
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/bounder/BounderService.class differ
diff --git a/bin/za/ac/sun/cs/green/service/bounder/BounderTest.class b/bin/za/ac/sun/cs/green/service/bounder/BounderTest.class
new file mode 100644
index 00000000..3a4ca385
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/bounder/BounderTest.class differ
diff --git a/bin/za/ac/sun/cs/green/service/canonizer/ModelCanonizerService.class b/bin/za/ac/sun/cs/green/service/canonizer/ModelCanonizerService.class
new file mode 100644
index 00000000..14df4bc9
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/canonizer/ModelCanonizerService.class differ
diff --git a/bin/za/ac/sun/cs/green/service/canonizer/SATCanonizerService$1.class b/bin/za/ac/sun/cs/green/service/canonizer/SATCanonizerService$1.class
new file mode 100644
index 00000000..67de5895
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/canonizer/SATCanonizerService$1.class differ
diff --git a/bin/za/ac/sun/cs/green/service/canonizer/SATCanonizerService$CanonizationVisitor.class b/bin/za/ac/sun/cs/green/service/canonizer/SATCanonizerService$CanonizationVisitor.class
new file mode 100644
index 00000000..809ac9b5
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/canonizer/SATCanonizerService$CanonizationVisitor.class differ
diff --git a/bin/za/ac/sun/cs/green/service/canonizer/SATCanonizerService$OrderingVisitor.class b/bin/za/ac/sun/cs/green/service/canonizer/SATCanonizerService$OrderingVisitor.class
new file mode 100644
index 00000000..7c865483
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/canonizer/SATCanonizerService$OrderingVisitor.class differ
diff --git a/bin/za/ac/sun/cs/green/service/canonizer/SATCanonizerService$Renamer.class b/bin/za/ac/sun/cs/green/service/canonizer/SATCanonizerService$Renamer.class
new file mode 100644
index 00000000..e4654b47
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/canonizer/SATCanonizerService$Renamer.class differ
diff --git a/bin/za/ac/sun/cs/green/service/canonizer/SATCanonizerService.class b/bin/za/ac/sun/cs/green/service/canonizer/SATCanonizerService.class
new file mode 100644
index 00000000..ec618692
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/canonizer/SATCanonizerService.class differ
diff --git a/bin/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.class b/bin/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.class
new file mode 100644
index 00000000..1ef46c91
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest.class differ
diff --git a/bin/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest2.class b/bin/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest2.class
new file mode 100644
index 00000000..ec037ba3
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/canonizer/SATCanonizerTest2.class differ
diff --git a/bin/za/ac/sun/cs/green/service/canonizer/SATLeafCanonizerService.class b/bin/za/ac/sun/cs/green/service/canonizer/SATLeafCanonizerService.class
new file mode 100644
index 00000000..ca28a039
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/canonizer/SATLeafCanonizerService.class differ
diff --git a/bin/za/ac/sun/cs/green/service/choco/ChocoTranslator$1.class b/bin/za/ac/sun/cs/green/service/choco/ChocoTranslator$1.class
new file mode 100644
index 00000000..e6f20566
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/choco/ChocoTranslator$1.class differ
diff --git a/bin/za/ac/sun/cs/green/service/choco/ChocoTranslator.class b/bin/za/ac/sun/cs/green/service/choco/ChocoTranslator.class
new file mode 100644
index 00000000..f8c345ce
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/choco/ChocoTranslator.class differ
diff --git a/bin/za/ac/sun/cs/green/service/choco/ModelChocoService.class b/bin/za/ac/sun/cs/green/service/choco/ModelChocoService.class
new file mode 100644
index 00000000..7ca24c2b
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/choco/ModelChocoService.class differ
diff --git a/bin/za/ac/sun/cs/green/service/choco/ModelChocoTest.class b/bin/za/ac/sun/cs/green/service/choco/ModelChocoTest.class
new file mode 100644
index 00000000..0af429fc
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/choco/ModelChocoTest.class differ
diff --git a/bin/za/ac/sun/cs/green/service/choco/SATChocoService.class b/bin/za/ac/sun/cs/green/service/choco/SATChocoService.class
new file mode 100644
index 00000000..f9ea3a1b
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/choco/SATChocoService.class differ
diff --git a/bin/za/ac/sun/cs/green/service/choco/SATChocoTest.class b/bin/za/ac/sun/cs/green/service/choco/SATChocoTest.class
new file mode 100644
index 00000000..b49c226b
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/choco/SATChocoTest.class differ
diff --git a/bin/za/ac/sun/cs/green/service/choco/TranslatorUnsupportedOperation.class b/bin/za/ac/sun/cs/green/service/choco/TranslatorUnsupportedOperation.class
new file mode 100644
index 00000000..64156b72
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/choco/TranslatorUnsupportedOperation.class differ
diff --git a/bin/za/ac/sun/cs/green/service/choco3/Choco3Translator$1.class b/bin/za/ac/sun/cs/green/service/choco3/Choco3Translator$1.class
new file mode 100644
index 00000000..dc46dbfd
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/choco3/Choco3Translator$1.class differ
diff --git a/bin/za/ac/sun/cs/green/service/choco3/Choco3Translator.class b/bin/za/ac/sun/cs/green/service/choco3/Choco3Translator.class
new file mode 100644
index 00000000..ef6996e5
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/choco3/Choco3Translator.class differ
diff --git a/bin/za/ac/sun/cs/green/service/choco3/ModelChoco3Service.class b/bin/za/ac/sun/cs/green/service/choco3/ModelChoco3Service.class
new file mode 100644
index 00000000..74a34512
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/choco3/ModelChoco3Service.class differ
diff --git a/bin/za/ac/sun/cs/green/service/choco3/ModelChoco3Test.class b/bin/za/ac/sun/cs/green/service/choco3/ModelChoco3Test.class
new file mode 100644
index 00000000..82bfd25c
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/choco3/ModelChoco3Test.class differ
diff --git a/bin/za/ac/sun/cs/green/service/choco3/ModelChoco3Test2.class b/bin/za/ac/sun/cs/green/service/choco3/ModelChoco3Test2.class
new file mode 100644
index 00000000..713c8624
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/choco3/ModelChoco3Test2.class differ
diff --git a/bin/za/ac/sun/cs/green/service/choco3/SATChoco3Service.class b/bin/za/ac/sun/cs/green/service/choco3/SATChoco3Service.class
new file mode 100644
index 00000000..586ac296
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/choco3/SATChoco3Service.class differ
diff --git a/bin/za/ac/sun/cs/green/service/choco3/SATChoco3Test.class b/bin/za/ac/sun/cs/green/service/choco3/SATChoco3Test.class
new file mode 100644
index 00000000..c9c2f038
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/choco3/SATChoco3Test.class differ
diff --git a/bin/za/ac/sun/cs/green/service/choco3/TranslatorUnsupportedOperation.class b/bin/za/ac/sun/cs/green/service/choco3/TranslatorUnsupportedOperation.class
new file mode 100644
index 00000000..d9b93bf1
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/choco3/TranslatorUnsupportedOperation.class differ
diff --git a/bin/za/ac/sun/cs/green/service/cvc3/SATCVC3Service$1.class b/bin/za/ac/sun/cs/green/service/cvc3/SATCVC3Service$1.class
new file mode 100644
index 00000000..cbcc87ec
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/cvc3/SATCVC3Service$1.class differ
diff --git a/bin/za/ac/sun/cs/green/service/cvc3/SATCVC3Service$Translator.class b/bin/za/ac/sun/cs/green/service/cvc3/SATCVC3Service$Translator.class
new file mode 100644
index 00000000..2b86934b
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/cvc3/SATCVC3Service$Translator.class differ
diff --git a/bin/za/ac/sun/cs/green/service/cvc3/SATCVC3Service$TranslatorUnsupportedOperation.class b/bin/za/ac/sun/cs/green/service/cvc3/SATCVC3Service$TranslatorUnsupportedOperation.class
new file mode 100644
index 00000000..77504ca6
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/cvc3/SATCVC3Service$TranslatorUnsupportedOperation.class differ
diff --git a/bin/za/ac/sun/cs/green/service/cvc3/SATCVC3Service.class b/bin/za/ac/sun/cs/green/service/cvc3/SATCVC3Service.class
new file mode 100644
index 00000000..1dd3efa5
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/cvc3/SATCVC3Service.class differ
diff --git a/bin/za/ac/sun/cs/green/service/cvc3/SATCVC3Test.class b/bin/za/ac/sun/cs/green/service/cvc3/SATCVC3Test.class
new file mode 100644
index 00000000..29c22d7d
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/cvc3/SATCVC3Test.class differ
diff --git a/bin/za/ac/sun/cs/green/service/factorizer/ComplexModelFactorizerTest.class b/bin/za/ac/sun/cs/green/service/factorizer/ComplexModelFactorizerTest.class
new file mode 100644
index 00000000..e4d1f14a
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/factorizer/ComplexModelFactorizerTest.class differ
diff --git a/bin/za/ac/sun/cs/green/service/factorizer/ComplexSATFactorizerTest.class b/bin/za/ac/sun/cs/green/service/factorizer/ComplexSATFactorizerTest.class
new file mode 100644
index 00000000..44eddf63
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/factorizer/ComplexSATFactorizerTest.class differ
diff --git a/bin/za/ac/sun/cs/green/service/factorizer/CountFactorizerService.class b/bin/za/ac/sun/cs/green/service/factorizer/CountFactorizerService.class
new file mode 100644
index 00000000..50732f15
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/factorizer/CountFactorizerService.class differ
diff --git a/bin/za/ac/sun/cs/green/service/factorizer/FactorExpression$Collector.class b/bin/za/ac/sun/cs/green/service/factorizer/FactorExpression$Collector.class
new file mode 100644
index 00000000..ae96cd4f
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/factorizer/FactorExpression$Collector.class differ
diff --git a/bin/za/ac/sun/cs/green/service/factorizer/FactorExpression.class b/bin/za/ac/sun/cs/green/service/factorizer/FactorExpression.class
new file mode 100644
index 00000000..631c8c89
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/factorizer/FactorExpression.class differ
diff --git a/bin/za/ac/sun/cs/green/service/factorizer/FactoredConstraintTest.class b/bin/za/ac/sun/cs/green/service/factorizer/FactoredConstraintTest.class
new file mode 100644
index 00000000..243fc8f8
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/factorizer/FactoredConstraintTest.class differ
diff --git a/bin/za/ac/sun/cs/green/service/factorizer/ModelFactorizerService.class b/bin/za/ac/sun/cs/green/service/factorizer/ModelFactorizerService.class
new file mode 100644
index 00000000..932ace35
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/factorizer/ModelFactorizerService.class differ
diff --git a/bin/za/ac/sun/cs/green/service/factorizer/SATFactorizerService.class b/bin/za/ac/sun/cs/green/service/factorizer/SATFactorizerService.class
new file mode 100644
index 00000000..da8eba88
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/factorizer/SATFactorizerService.class differ
diff --git a/bin/za/ac/sun/cs/green/service/factorizer/SATFactorizerTest.class b/bin/za/ac/sun/cs/green/service/factorizer/SATFactorizerTest.class
new file mode 100644
index 00000000..35254fd2
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/factorizer/SATFactorizerTest.class differ
diff --git a/bin/za/ac/sun/cs/green/service/latte/CountLattEService$HMatrix$1.class b/bin/za/ac/sun/cs/green/service/latte/CountLattEService$HMatrix$1.class
new file mode 100644
index 00000000..2f923f32
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/latte/CountLattEService$HMatrix$1.class differ
diff --git a/bin/za/ac/sun/cs/green/service/latte/CountLattEService$HMatrix.class b/bin/za/ac/sun/cs/green/service/latte/CountLattEService$HMatrix.class
new file mode 100644
index 00000000..5d3b9357
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/latte/CountLattEService$HMatrix.class differ
diff --git a/bin/za/ac/sun/cs/green/service/latte/CountLattEService$HRow.class b/bin/za/ac/sun/cs/green/service/latte/CountLattEService$HRow.class
new file mode 100644
index 00000000..05e83c1b
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/latte/CountLattEService$HRow.class differ
diff --git a/bin/za/ac/sun/cs/green/service/latte/CountLattEService$Subsetter.class b/bin/za/ac/sun/cs/green/service/latte/CountLattEService$Subsetter.class
new file mode 100644
index 00000000..5892b46c
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/latte/CountLattEService$Subsetter.class differ
diff --git a/bin/za/ac/sun/cs/green/service/latte/CountLattEService.class b/bin/za/ac/sun/cs/green/service/latte/CountLattEService.class
new file mode 100644
index 00000000..8fda9da0
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/latte/CountLattEService.class differ
diff --git a/bin/za/ac/sun/cs/green/service/latte/CountLattETest.class b/bin/za/ac/sun/cs/green/service/latte/CountLattETest.class
new file mode 100644
index 00000000..efc1ade9
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/latte/CountLattETest.class differ
diff --git a/bin/za/ac/sun/cs/green/service/latte/CountLattEWithBounderTest.class b/bin/za/ac/sun/cs/green/service/latte/CountLattEWithBounderTest.class
new file mode 100644
index 00000000..5bd22eec
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/latte/CountLattEWithBounderTest.class differ
diff --git a/bin/za/ac/sun/cs/green/service/renamer/RenamerService$Renamer.class b/bin/za/ac/sun/cs/green/service/renamer/RenamerService$Renamer.class
new file mode 100644
index 00000000..4083dcc4
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/renamer/RenamerService$Renamer.class differ
diff --git a/bin/za/ac/sun/cs/green/service/renamer/RenamerService$RenamerVisitor.class b/bin/za/ac/sun/cs/green/service/renamer/RenamerService$RenamerVisitor.class
new file mode 100644
index 00000000..b1a13d76
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/renamer/RenamerService$RenamerVisitor.class differ
diff --git a/bin/za/ac/sun/cs/green/service/renamer/RenamerService.class b/bin/za/ac/sun/cs/green/service/renamer/RenamerService.class
new file mode 100644
index 00000000..0d6e121b
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/renamer/RenamerService.class differ
diff --git a/bin/za/ac/sun/cs/green/service/simplify/ConstantPropagation$1.class b/bin/za/ac/sun/cs/green/service/simplify/ConstantPropagation$1.class
new file mode 100644
index 00000000..c643df50
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/simplify/ConstantPropagation$1.class differ
diff --git a/bin/za/ac/sun/cs/green/service/simplify/ConstantPropagation$CanonizationVisitor.class b/bin/za/ac/sun/cs/green/service/simplify/ConstantPropagation$CanonizationVisitor.class
new file mode 100644
index 00000000..09aa8cb0
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/simplify/ConstantPropagation$CanonizationVisitor.class differ
diff --git a/bin/za/ac/sun/cs/green/service/simplify/ConstantPropagation$ExchangeVisitor.class b/bin/za/ac/sun/cs/green/service/simplify/ConstantPropagation$ExchangeVisitor.class
new file mode 100644
index 00000000..47efd07d
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/simplify/ConstantPropagation$ExchangeVisitor.class differ
diff --git a/bin/za/ac/sun/cs/green/service/simplify/ConstantPropagation$OrderingVisitor.class b/bin/za/ac/sun/cs/green/service/simplify/ConstantPropagation$OrderingVisitor.class
new file mode 100644
index 00000000..58a7c1f2
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/simplify/ConstantPropagation$OrderingVisitor.class differ
diff --git a/bin/za/ac/sun/cs/green/service/simplify/ConstantPropagation$Renamer.class b/bin/za/ac/sun/cs/green/service/simplify/ConstantPropagation$Renamer.class
new file mode 100644
index 00000000..b0ba5f2f
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/simplify/ConstantPropagation$Renamer.class differ
diff --git a/bin/za/ac/sun/cs/green/service/simplify/ConstantPropagation.class b/bin/za/ac/sun/cs/green/service/simplify/ConstantPropagation.class
new file mode 100644
index 00000000..8c8f7472
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/simplify/ConstantPropagation.class differ
diff --git a/bin/za/ac/sun/cs/green/service/simplify/OnlyConstantPropogationTest.class b/bin/za/ac/sun/cs/green/service/simplify/OnlyConstantPropogationTest.class
new file mode 100644
index 00000000..4c6ca5a7
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/simplify/OnlyConstantPropogationTest.class differ
diff --git a/bin/za/ac/sun/cs/green/service/simplify/SimplificationConstantPropogationTest.class b/bin/za/ac/sun/cs/green/service/simplify/SimplificationConstantPropogationTest.class
new file mode 100644
index 00000000..841979f9
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/simplify/SimplificationConstantPropogationTest.class differ
diff --git a/bin/za/ac/sun/cs/green/service/sink/FactorSinkService.class b/bin/za/ac/sun/cs/green/service/sink/FactorSinkService.class
new file mode 100644
index 00000000..f4bcda9d
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/sink/FactorSinkService.class differ
diff --git a/bin/za/ac/sun/cs/green/service/sink/SinkService.class b/bin/za/ac/sun/cs/green/service/sink/SinkService.class
new file mode 100644
index 00000000..cf2f7c4f
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/sink/SinkService.class differ
diff --git a/bin/za/ac/sun/cs/green/service/slicer/ParallelSATSlicerTest.class b/bin/za/ac/sun/cs/green/service/slicer/ParallelSATSlicerTest.class
new file mode 100644
index 00000000..e88430c5
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/slicer/ParallelSATSlicerTest.class differ
diff --git a/bin/za/ac/sun/cs/green/service/slicer/SATFactorSlicerService.class b/bin/za/ac/sun/cs/green/service/slicer/SATFactorSlicerService.class
new file mode 100644
index 00000000..d9b2ef33
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/slicer/SATFactorSlicerService.class differ
diff --git a/bin/za/ac/sun/cs/green/service/slicer/SATFactorSlicerTest.class b/bin/za/ac/sun/cs/green/service/slicer/SATFactorSlicerTest.class
new file mode 100644
index 00000000..5bb017d1
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/slicer/SATFactorSlicerTest.class differ
diff --git a/bin/za/ac/sun/cs/green/service/slicer/SATSlicerService.class b/bin/za/ac/sun/cs/green/service/slicer/SATSlicerService.class
new file mode 100644
index 00000000..fd77ebb6
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/slicer/SATSlicerService.class differ
diff --git a/bin/za/ac/sun/cs/green/service/slicer/SATSlicerTest.class b/bin/za/ac/sun/cs/green/service/slicer/SATSlicerTest.class
new file mode 100644
index 00000000..811e25cb
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/slicer/SATSlicerTest.class differ
diff --git a/bin/za/ac/sun/cs/green/service/slicer/Slicer$Collector.class b/bin/za/ac/sun/cs/green/service/slicer/Slicer$Collector.class
new file mode 100644
index 00000000..dcc1aa51
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/slicer/Slicer$Collector.class differ
diff --git a/bin/za/ac/sun/cs/green/service/slicer/Slicer$Enqueuer.class b/bin/za/ac/sun/cs/green/service/slicer/Slicer$Enqueuer.class
new file mode 100644
index 00000000..250ed05f
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/slicer/Slicer$Enqueuer.class differ
diff --git a/bin/za/ac/sun/cs/green/service/slicer/Slicer.class b/bin/za/ac/sun/cs/green/service/slicer/Slicer.class
new file mode 100644
index 00000000..e6e477d5
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/slicer/Slicer.class differ
diff --git a/bin/za/ac/sun/cs/green/service/smtlib/SATSMTLIBService$1.class b/bin/za/ac/sun/cs/green/service/smtlib/SATSMTLIBService$1.class
new file mode 100644
index 00000000..a19da402
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/smtlib/SATSMTLIBService$1.class differ
diff --git a/bin/za/ac/sun/cs/green/service/smtlib/SATSMTLIBService$Translator.class b/bin/za/ac/sun/cs/green/service/smtlib/SATSMTLIBService$Translator.class
new file mode 100644
index 00000000..080a0c8e
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/smtlib/SATSMTLIBService$Translator.class differ
diff --git a/bin/za/ac/sun/cs/green/service/smtlib/SATSMTLIBService$TranslatorPair.class b/bin/za/ac/sun/cs/green/service/smtlib/SATSMTLIBService$TranslatorPair.class
new file mode 100644
index 00000000..88c19d69
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/smtlib/SATSMTLIBService$TranslatorPair.class differ
diff --git a/bin/za/ac/sun/cs/green/service/smtlib/SATSMTLIBService$TranslatorUnsupportedOperation.class b/bin/za/ac/sun/cs/green/service/smtlib/SATSMTLIBService$TranslatorUnsupportedOperation.class
new file mode 100644
index 00000000..e9ec1727
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/smtlib/SATSMTLIBService$TranslatorUnsupportedOperation.class differ
diff --git a/bin/za/ac/sun/cs/green/service/smtlib/SATSMTLIBService.class b/bin/za/ac/sun/cs/green/service/smtlib/SATSMTLIBService.class
new file mode 100644
index 00000000..23321596
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/smtlib/SATSMTLIBService.class differ
diff --git a/bin/za/ac/sun/cs/green/service/z3/ModelZ3JavaService.class b/bin/za/ac/sun/cs/green/service/z3/ModelZ3JavaService.class
new file mode 100644
index 00000000..cf6a00a3
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/z3/ModelZ3JavaService.class differ
diff --git a/bin/za/ac/sun/cs/green/service/z3/ModelZ3JavaTest.class b/bin/za/ac/sun/cs/green/service/z3/ModelZ3JavaTest.class
new file mode 100644
index 00000000..a3cbc98e
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/z3/ModelZ3JavaTest.class differ
diff --git a/bin/za/ac/sun/cs/green/service/z3/ModelZ3JavaTest2.class b/bin/za/ac/sun/cs/green/service/z3/ModelZ3JavaTest2.class
new file mode 100644
index 00000000..7e9a430a
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/z3/ModelZ3JavaTest2.class differ
diff --git a/bin/za/ac/sun/cs/green/service/z3/SATZ3CompareTest.class b/bin/za/ac/sun/cs/green/service/z3/SATZ3CompareTest.class
new file mode 100644
index 00000000..3cd36075
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/z3/SATZ3CompareTest.class differ
diff --git a/bin/za/ac/sun/cs/green/service/z3/SATZ3JavaService$Z3Wrapper.class b/bin/za/ac/sun/cs/green/service/z3/SATZ3JavaService$Z3Wrapper.class
new file mode 100644
index 00000000..5aa5e260
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/z3/SATZ3JavaService$Z3Wrapper.class differ
diff --git a/bin/za/ac/sun/cs/green/service/z3/SATZ3JavaService.class b/bin/za/ac/sun/cs/green/service/z3/SATZ3JavaService.class
new file mode 100644
index 00000000..ad5cce96
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/z3/SATZ3JavaService.class differ
diff --git a/bin/za/ac/sun/cs/green/service/z3/SATZ3JavaTest.class b/bin/za/ac/sun/cs/green/service/z3/SATZ3JavaTest.class
new file mode 100644
index 00000000..5cf8c378
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/z3/SATZ3JavaTest.class differ
diff --git a/bin/za/ac/sun/cs/green/service/z3/SATZ3Service.class b/bin/za/ac/sun/cs/green/service/z3/SATZ3Service.class
new file mode 100644
index 00000000..18fe7dbc
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/z3/SATZ3Service.class differ
diff --git a/bin/za/ac/sun/cs/green/service/z3/SATZ3Test.class b/bin/za/ac/sun/cs/green/service/z3/SATZ3Test.class
new file mode 100644
index 00000000..724feecf
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/z3/SATZ3Test.class differ
diff --git a/bin/za/ac/sun/cs/green/service/z3/TranslatorUnsupportedOperation.class b/bin/za/ac/sun/cs/green/service/z3/TranslatorUnsupportedOperation.class
new file mode 100644
index 00000000..563c88b4
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/z3/TranslatorUnsupportedOperation.class differ
diff --git a/bin/za/ac/sun/cs/green/service/z3/Z3JavaTranslator$1.class b/bin/za/ac/sun/cs/green/service/z3/Z3JavaTranslator$1.class
new file mode 100644
index 00000000..7affb9ec
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/z3/Z3JavaTranslator$1.class differ
diff --git a/bin/za/ac/sun/cs/green/service/z3/Z3JavaTranslator.class b/bin/za/ac/sun/cs/green/service/z3/Z3JavaTranslator.class
new file mode 100644
index 00000000..daf7ae96
Binary files /dev/null and b/bin/za/ac/sun/cs/green/service/z3/Z3JavaTranslator.class differ
diff --git a/bin/za/ac/sun/cs/green/store/BasicStore.class b/bin/za/ac/sun/cs/green/store/BasicStore.class
new file mode 100644
index 00000000..73125575
Binary files /dev/null and b/bin/za/ac/sun/cs/green/store/BasicStore.class differ
diff --git a/bin/za/ac/sun/cs/green/store/NullStore.class b/bin/za/ac/sun/cs/green/store/NullStore.class
new file mode 100644
index 00000000..979e3863
Binary files /dev/null and b/bin/za/ac/sun/cs/green/store/NullStore.class differ
diff --git a/bin/za/ac/sun/cs/green/store/Store.class b/bin/za/ac/sun/cs/green/store/Store.class
new file mode 100644
index 00000000..c62b2d2b
Binary files /dev/null and b/bin/za/ac/sun/cs/green/store/Store.class differ
diff --git a/bin/za/ac/sun/cs/green/store/redis/RedisStore.class b/bin/za/ac/sun/cs/green/store/redis/RedisStore.class
new file mode 100644
index 00000000..3416dd4d
Binary files /dev/null and b/bin/za/ac/sun/cs/green/store/redis/RedisStore.class differ
diff --git a/bin/za/ac/sun/cs/green/taskmanager/ParallelTaskManager$Task.class b/bin/za/ac/sun/cs/green/taskmanager/ParallelTaskManager$Task.class
new file mode 100644
index 00000000..37276276
Binary files /dev/null and b/bin/za/ac/sun/cs/green/taskmanager/ParallelTaskManager$Task.class differ
diff --git a/bin/za/ac/sun/cs/green/taskmanager/ParallelTaskManager.class b/bin/za/ac/sun/cs/green/taskmanager/ParallelTaskManager.class
new file mode 100644
index 00000000..98797b23
Binary files /dev/null and b/bin/za/ac/sun/cs/green/taskmanager/ParallelTaskManager.class differ
diff --git a/bin/za/ac/sun/cs/green/taskmanager/SerialTaskManager.class b/bin/za/ac/sun/cs/green/taskmanager/SerialTaskManager.class
new file mode 100644
index 00000000..c9f6e89c
Binary files /dev/null and b/bin/za/ac/sun/cs/green/taskmanager/SerialTaskManager.class differ
diff --git a/bin/za/ac/sun/cs/green/taskmanager/TaskManager.class b/bin/za/ac/sun/cs/green/taskmanager/TaskManager.class
new file mode 100644
index 00000000..cf5194fa
Binary files /dev/null and b/bin/za/ac/sun/cs/green/taskmanager/TaskManager.class differ
diff --git a/bin/za/ac/sun/cs/green/util/Base64.class b/bin/za/ac/sun/cs/green/util/Base64.class
new file mode 100644
index 00000000..28260219
Binary files /dev/null and b/bin/za/ac/sun/cs/green/util/Base64.class differ
diff --git a/bin/za/ac/sun/cs/green/util/Configuration$ParseException.class b/bin/za/ac/sun/cs/green/util/Configuration$ParseException.class
new file mode 100644
index 00000000..e4ce54ea
Binary files /dev/null and b/bin/za/ac/sun/cs/green/util/Configuration$ParseException.class differ
diff --git a/bin/za/ac/sun/cs/green/util/Configuration$ParseTree.class b/bin/za/ac/sun/cs/green/util/Configuration$ParseTree.class
new file mode 100644
index 00000000..f911fd72
Binary files /dev/null and b/bin/za/ac/sun/cs/green/util/Configuration$ParseTree.class differ
diff --git a/bin/za/ac/sun/cs/green/util/Configuration$Parser.class b/bin/za/ac/sun/cs/green/util/Configuration$Parser.class
new file mode 100644
index 00000000..10d876fb
Binary files /dev/null and b/bin/za/ac/sun/cs/green/util/Configuration$Parser.class differ
diff --git a/bin/za/ac/sun/cs/green/util/Configuration$Scanner.class b/bin/za/ac/sun/cs/green/util/Configuration$Scanner.class
new file mode 100644
index 00000000..c1d651e8
Binary files /dev/null and b/bin/za/ac/sun/cs/green/util/Configuration$Scanner.class differ
diff --git a/bin/za/ac/sun/cs/green/util/Configuration$Token.class b/bin/za/ac/sun/cs/green/util/Configuration$Token.class
new file mode 100644
index 00000000..5ffab9e2
Binary files /dev/null and b/bin/za/ac/sun/cs/green/util/Configuration$Token.class differ
diff --git a/bin/za/ac/sun/cs/green/util/Configuration.class b/bin/za/ac/sun/cs/green/util/Configuration.class
new file mode 100644
index 00000000..499e989f
Binary files /dev/null and b/bin/za/ac/sun/cs/green/util/Configuration.class differ
diff --git a/bin/za/ac/sun/cs/green/util/DummyTaskManager.class b/bin/za/ac/sun/cs/green/util/DummyTaskManager.class
new file mode 100644
index 00000000..389b3709
Binary files /dev/null and b/bin/za/ac/sun/cs/green/util/DummyTaskManager.class differ
diff --git a/bin/za/ac/sun/cs/green/util/Misc.class b/bin/za/ac/sun/cs/green/util/Misc.class
new file mode 100644
index 00000000..7a018bc7
Binary files /dev/null and b/bin/za/ac/sun/cs/green/util/Misc.class differ
diff --git a/bin/za/ac/sun/cs/green/util/NullLogger.class b/bin/za/ac/sun/cs/green/util/NullLogger.class
new file mode 100644
index 00000000..e42f57c9
Binary files /dev/null and b/bin/za/ac/sun/cs/green/util/NullLogger.class differ
diff --git a/bin/za/ac/sun/cs/green/util/ParallelSATTest.class b/bin/za/ac/sun/cs/green/util/ParallelSATTest.class
new file mode 100644
index 00000000..be59b014
Binary files /dev/null and b/bin/za/ac/sun/cs/green/util/ParallelSATTest.class differ
diff --git a/bin/za/ac/sun/cs/green/util/Reporter.class b/bin/za/ac/sun/cs/green/util/Reporter.class
new file mode 100644
index 00000000..762fdddc
Binary files /dev/null and b/bin/za/ac/sun/cs/green/util/Reporter.class differ
diff --git a/bin/za/ac/sun/cs/green/util/SetServiceTest.class b/bin/za/ac/sun/cs/green/util/SetServiceTest.class
new file mode 100644
index 00000000..955a4f75
Binary files /dev/null and b/bin/za/ac/sun/cs/green/util/SetServiceTest.class differ
diff --git a/bin/za/ac/sun/cs/green/util/SetTaskManagerTest.class b/bin/za/ac/sun/cs/green/util/SetTaskManagerTest.class
new file mode 100644
index 00000000..b229d5db
Binary files /dev/null and b/bin/za/ac/sun/cs/green/util/SetTaskManagerTest.class differ
diff --git a/build.xml b/build.xml
index 0c29bed8..59adc2db 100644
--- a/build.xml
+++ b/build.xml
@@ -42,6 +42,7 @@
+