diff --git a/src/test/java/pico/ImmutabilityReImInferenceTest.java b/src/test/java/pico/ImmutabilityReImInferenceTest.java
new file mode 100644
index 0000000..c72cffa
--- /dev/null
+++ b/src/test/java/pico/ImmutabilityReImInferenceTest.java
@@ -0,0 +1,42 @@
+package pico;
+
+import checkers.inference.test.CFInferenceTest;
+import org.checkerframework.framework.test.TestUtilities;
+import org.checkerframework.javacutil.Pair;
+import org.junit.Ignore;
+import org.junit.runners.Parameterized.Parameters;
+import pico.inference.PICOInferenceChecker;
+import pico.inference.solver.PICOSolverEngine;
+
+import java.io.File;
+import java.util.ArrayList;
+import java.util.Arrays;
+import java.util.List;
+
+@SuppressWarnings("initialization")
+public class ImmutabilityReImInferenceTest extends CFInferenceTest {
+
+    public ImmutabilityReImInferenceTest(File testFile) {
+        super(testFile, PICOInferenceChecker.class, "",
+              "-Anomsgtext",
+                "-Astubs=src/main/java/pico/inference/jdk.astub",
+                "-d", "testdata/reiminfer");
+    }
+
+    @Override
+    public Pair<String, List<String>> getSolverNameAndOptions() {
+        return Pair.of(PICOSolverEngine.class.getCanonicalName(),
+                new ArrayList<>(Arrays.asList("useGraph=false", "collectStatistic=true")));
+    }
+
+    @Override
+    public boolean useHacks() {
+        return true;
+    }
+
+    @Parameters
+    public static List<File> getTestFiles(){
+        //InferenceTestUtilities.findAllSystemTests();
+        return new ArrayList<>(TestUtilities.findRelativeNestedJavaFiles("testinput", "reiminfer"));
+    }
+}
diff --git a/src/test/java/pico/ImmutabilityTypecheckGlacierTest.java b/src/test/java/pico/ImmutabilityTypecheckGlacierTest.java
new file mode 100644
index 0000000..eb7857a
--- /dev/null
+++ b/src/test/java/pico/ImmutabilityTypecheckGlacierTest.java
@@ -0,0 +1,23 @@
+package pico;
+
+import org.checkerframework.framework.test.CheckerFrameworkPerFileTest;
+import org.checkerframework.framework.test.TestUtilities;
+import org.junit.Ignore;
+import org.junit.runners.Parameterized.Parameters;
+import pico.typecheck.PICOChecker;
+
+import java.io.File;
+import java.util.ArrayList;
+import java.util.List;
+
+public class ImmutabilityTypecheckGlacierTest extends CheckerFrameworkPerFileTest {
+    public ImmutabilityTypecheckGlacierTest(File testFile) {
+        super(testFile, PICOChecker.class, "", "-Anomsgtext",
+                "-Anocheckjdk", "-d", "testTmp/glacier");
+    }
+
+    @Parameters
+    public static List<File> getTestFiles(){
+        return new ArrayList<>(TestUtilities.findRelativeNestedJavaFiles("testinput", "glacier"));
+    }
+}
diff --git a/testinput/glacier/ArrayClone.java b/testinput/glacier/ArrayClone.java
new file mode 100644
index 0000000..e9a16ab
--- /dev/null
+++ b/testinput/glacier/ArrayClone.java
@@ -0,0 +1,7 @@
+// Change to PICO; array clone adaption.
+import qual.*;
+
+public class ArrayClone {
+    @Immutable Object @Immutable [] array = new @Immutable Object  @Immutable [0];
+    @Immutable Object @Immutable [] arrayClone = array.clone();
+}
\ No newline at end of file
diff --git a/testinput/glacier/ArrayCopy.java b/testinput/glacier/ArrayCopy.java
new file mode 100644
index 0000000..ba4e8f4
--- /dev/null
+++ b/testinput/glacier/ArrayCopy.java
@@ -0,0 +1,18 @@
+// @skip-test
+// Typecheck: Failed
+// Cause: checker cannot get clone() decl from stub! Decl receiver and return type get defaulted to mutable.
+// strange enough, seems other signatures are got from stubs.
+import qual.Immutable;
+
+
+public class ArrayCopy {
+    public void takeArray(@Immutable Object @Immutable [] array) {
+    }
+
+    public void passArray() {
+        @Immutable Object array[] = new @Immutable Object[5];
+
+        takeArray(array.clone());
+    }
+
+}
\ No newline at end of file
diff --git a/testinput/glacier/ArrayParameter.java b/testinput/glacier/ArrayParameter.java
new file mode 100644
index 0000000..81f77b4
--- /dev/null
+++ b/testinput/glacier/ArrayParameter.java
@@ -0,0 +1,22 @@
+import qual.*;
+import java.util.Arrays;
+
+
+class Array {
+    public static <T> T[] add(final T @Readonly[] array, final T entry) {
+        final int s = array.length;
+        final T[] t = Arrays.copyOf(array, s + 1);
+        t[s] = entry;
+        return t;
+    }
+}
+
+
+public class ArrayParameter {
+    final @Immutable Object @Immutable [] keys = new @Immutable Object @Immutable [0];
+
+
+    public void passArray(@Immutable Object k) {
+        Array.add(keys, k);
+    }
+}
\ No newline at end of file
diff --git a/testinput/glacier/Arrays.java b/testinput/glacier/Arrays.java
new file mode 100644
index 0000000..3fde23c
--- /dev/null
+++ b/testinput/glacier/Arrays.java
@@ -0,0 +1,21 @@
+package glacier;
+
+public class Arrays {
+    int [] intArray;
+
+    public Arrays() {
+
+    }
+
+    public int[] getData() {
+        return intArray;
+    }
+
+    public byte[] getByteData() {
+        return new byte[0];
+    }
+
+    public void setData() {
+        intArray[0] = 42;
+    }
+}
\ No newline at end of file
diff --git a/testinput/glacier/BooleanSubtyping.java b/testinput/glacier/BooleanSubtyping.java
new file mode 100644
index 0000000..dcae5b7
--- /dev/null
+++ b/testinput/glacier/BooleanSubtyping.java
@@ -0,0 +1,16 @@
+public class BooleanSubtyping {
+    public enum CellType {
+        BLANK(3),
+        NUMBER(0);
+
+        private int value;
+        private CellType(int value) {
+            this.value = value;
+        }
+    }
+
+    public boolean foo() {
+        CellType cellType = CellType.BLANK;
+        return cellType == CellType.NUMBER;
+    }
+}
\ No newline at end of file
diff --git a/testinput/glacier/ClassGetName.java b/testinput/glacier/ClassGetName.java
new file mode 100644
index 0000000..ca11263
--- /dev/null
+++ b/testinput/glacier/ClassGetName.java
@@ -0,0 +1,6 @@
+public class ClassGetName {
+    public String foo() {
+        Number num = null;
+        return num.getClass().getName();
+    }
+}
\ No newline at end of file
diff --git a/testinput/glacier/ClassReturn.java b/testinput/glacier/ClassReturn.java
new file mode 100644
index 0000000..25e23b4
--- /dev/null
+++ b/testinput/glacier/ClassReturn.java
@@ -0,0 +1,9 @@
+// typecheck: OK
+
+
+public class ClassReturn {
+    public ClassReturn getInstance() {
+        return new ClassReturn();
+    }
+
+}
\ No newline at end of file
diff --git a/testinput/glacier/ColorImpl.java b/testinput/glacier/ColorImpl.java
new file mode 100644
index 0000000..2ff6a09
--- /dev/null
+++ b/testinput/glacier/ColorImpl.java
@@ -0,0 +1,18 @@
+// @skip-test
+// Typecheck, Inference-TC: Failed
+// Cause: checker cannot get clone() decl from stub! Decl receiver and return type get defaulted to mutable.
+// strange enough, seems other signatures are got from stubs.
+import java.util.Arrays;
+import qual.Immutable;
+
+public class ColorImpl {
+    private byte @Immutable [] _rgb;
+    private byte [] _mutableRgb;
+
+    public int hashCode() {
+        // This should be OK, but will be an error until we have a @ReadOnly annotation.
+        Arrays.hashCode(_mutableRgb);
+
+        return Arrays.hashCode(_rgb);
+    }
+}
\ No newline at end of file
diff --git a/testinput/glacier/CompareTo.java b/testinput/glacier/CompareTo.java
new file mode 100644
index 0000000..b1b9a1c
--- /dev/null
+++ b/testinput/glacier/CompareTo.java
@@ -0,0 +1,11 @@
+package glacier;
+
+public class CompareTo {
+
+    public void foo() {
+        Object val1 = null;
+        Object val2 = null;
+        // Shouldn't give an error.
+        ((Boolean)val1).compareTo((Boolean)val2);
+    }
+}
\ No newline at end of file
diff --git a/testinput/glacier/ConflictingAnnotations.java b/testinput/glacier/ConflictingAnnotations.java
new file mode 100644
index 0000000..1729ae5
--- /dev/null
+++ b/testinput/glacier/ConflictingAnnotations.java
@@ -0,0 +1,33 @@
+import qual.*;
+
+@Immutable class ImmutClass {
+}
+
+@Mutable class MutableClass {
+}
+
+class DefaultMutableClass {
+}
+
+@Immutable interface ImmutInterface {
+}
+
+interface MutableInterface {
+}
+
+public class ConflictingAnnotations {
+    // ::error: (type.invalid.annotations.on.use)
+    @Mutable ImmutClass o1;
+
+    // ::error: (type.invalid.annotations.on.use)
+    @Immutable MutableClass o2;
+
+    // ::error: (type.invalid.annotations.on.use)
+    @Immutable DefaultMutableClass o3;
+
+    // ::error: (type.invalid.annotations.on.use)
+    @Mutable ImmutInterface i1;
+
+    // ::error: (type.invalid.annotations.on.use)
+    @Immutable MutableInterface i2;
+}
\ No newline at end of file
diff --git a/testinput/glacier/ConstructorAssignment.java b/testinput/glacier/ConstructorAssignment.java
new file mode 100644
index 0000000..4f9db96
--- /dev/null
+++ b/testinput/glacier/ConstructorAssignment.java
@@ -0,0 +1,24 @@
+package glacier;
+
+import qual.Immutable;
+
+public @Immutable class ConstructorAssignment {
+    public int x = 3; // static assignment is OK
+
+    ConstructorAssignment() {
+        x = 4; // constructor assignment is OK
+    }
+
+    void setX() {
+        // ::error: (illegal.field.write)
+        x = 5;
+    }
+}
+
+class OtherClass {
+    OtherClass() {
+        ConstructorAssignment c = new ConstructorAssignment();
+        // ::error: (illegal.field.write)
+        c.x = 6;
+    }
+}
\ No newline at end of file
diff --git a/testinput/glacier/EnumTest.java b/testinput/glacier/EnumTest.java
new file mode 100644
index 0000000..6d0b16a
--- /dev/null
+++ b/testinput/glacier/EnumTest.java
@@ -0,0 +1,19 @@
+package glacier;
+
+import qual.Immutable;
+
+@Immutable enum Underline{
+    NONE,
+    SINGLE,
+    DOUBLE,
+    SINGLE_ACCOUNTING,
+    DOUBLE_ACCOUNTING
+}
+
+public class EnumTest {
+    Underline u;
+
+    public void foo() {
+        u.ordinal();
+    }
+}
\ No newline at end of file
diff --git a/testinput/glacier/EqualsTest.java b/testinput/glacier/EqualsTest.java
new file mode 100644
index 0000000..50c6640
--- /dev/null
+++ b/testinput/glacier/EqualsTest.java
@@ -0,0 +1,23 @@
+// @skip-test
+package glacier;
+
+import qual.*;
+
+@Immutable public class EqualsTest {
+    @Override
+    public boolean equals(Object obj) {
+        if (this == obj)
+            return true;
+        return false;
+    }
+}
+
+class EqualsTest2 {
+    @Override
+    // ::error: (override.param.invalid)
+    public boolean equals(@Immutable Object obj) {
+        if (this == obj)
+            return true;
+        return false;
+    }
+}
\ No newline at end of file
diff --git a/testinput/glacier/FontImpl.java b/testinput/glacier/FontImpl.java
new file mode 100644
index 0000000..82a8f40
--- /dev/null
+++ b/testinput/glacier/FontImpl.java
@@ -0,0 +1,34 @@
+// Note: PICO defaults the class decal to RDM. Removing errors on line 26 and 30.
+
+import qual.*;
+
+@Immutable  interface SColor {
+}
+
+@Immutable abstract class AbstractColorAdv implements SColor {
+}
+
+// ::error: (type.invalid.annotations.on.use)
+class FI_ColorImpl extends AbstractColorAdv {
+    // Arguably it would be preferable for this to not be an error.
+    // ::error: (type.invalid.annotations.on.use)
+    public static final AbstractColorAdv BLACK = new FI_ColorImpl("#000000");
+
+    // PICO Note: adding this error.
+    // ::error: (super.invocation.invalid)
+    FI_ColorImpl(String fontColor) {
+
+    }
+}
+
+public class FontImpl {
+    FontImpl(String fontColor) {
+        // Arguably it would be preferable for this to not be an error.
+        // Removing error. PICO chose the preferable path.
+        SColor a = new FI_ColorImpl(fontColor);
+
+        // Arguably it would be preferable for this to not be an error either.
+        // Removing error. PICO chose the preferable path.
+        SColor c = fontColor != null ? new FI_ColorImpl(fontColor) : null;
+    }
+}
\ No newline at end of file
diff --git a/testinput/glacier/ImmutableArray.java b/testinput/glacier/ImmutableArray.java
new file mode 100644
index 0000000..631d6b2
--- /dev/null
+++ b/testinput/glacier/ImmutableArray.java
@@ -0,0 +1,16 @@
+import qual.Immutable;
+
+@SuppressWarnings("initialization")
+@Immutable class ImmutableArray {
+    private byte @Immutable [] _rgb;
+
+    private String @Immutable [] _strings;
+
+    // Immutable array of mutable objects is mutable.
+    // PICO allows shallow immutable array.
+    private java.util.Date @Immutable [] _dates;
+
+    // MaybeMutable array of primitives is mutable.
+    // PICO allows shallow immutable array.
+    private int [] _ints;
+}
\ No newline at end of file
diff --git a/testinput/glacier/ImmutableClassMutableInterface.java b/testinput/glacier/ImmutableClassMutableInterface.java
new file mode 100644
index 0000000..ab85fb1
--- /dev/null
+++ b/testinput/glacier/ImmutableClassMutableInterface.java
@@ -0,0 +1,14 @@
+import qual.*;
+
+@ReceiverDependantMutable
+interface ICMI_MutableInterface {};
+
+@Immutable public class ImmutableClassMutableInterface implements ICMI_MutableInterface {
+    public static void bar(ICMI_MutableInterface m) { };
+
+    public static void foo() {
+        ImmutableClassMutableInterface x = null;
+        bar(x);
+    }
+
+};
\ No newline at end of file
diff --git a/testinput/glacier/ImmutableCollection.java b/testinput/glacier/ImmutableCollection.java
new file mode 100644
index 0000000..11833d8
--- /dev/null
+++ b/testinput/glacier/ImmutableCollection.java
@@ -0,0 +1,11 @@
+// Update to PICO: add AbstractCollection to stub
+import qual.Immutable;
+
+import java.util.*;
+
+@Immutable
+public abstract class ImmutableCollection<E> extends AbstractCollection<E> {
+    public int getSize() {
+        return size();
+    }
+}
\ No newline at end of file
diff --git a/testinput/glacier/ImmutableConstructorInMutableClass.java b/testinput/glacier/ImmutableConstructorInMutableClass.java
new file mode 100644
index 0000000..143e3b5
--- /dev/null
+++ b/testinput/glacier/ImmutableConstructorInMutableClass.java
@@ -0,0 +1,15 @@
+package glacier;
+
+import qual.Immutable;
+
+
+
+public class ImmutableConstructorInMutableClass {
+    // :: error: (type.invalid.annotations.on.use)
+    public @Immutable ImmutableConstructorInMutableClass() {
+    }
+
+    public void aMethod() {
+
+    }
+}
\ No newline at end of file
diff --git a/testinput/glacier/ImmutableInterfaceClass.java b/testinput/glacier/ImmutableInterfaceClass.java
new file mode 100644
index 0000000..1e888fc
--- /dev/null
+++ b/testinput/glacier/ImmutableInterfaceClass.java
@@ -0,0 +1,11 @@
+package glacier;
+
+import qual.Immutable;
+
+
+@Immutable interface ImmutableInterface {
+}
+
+public @Immutable class ImmutableInterfaceClass implements ImmutableInterface {
+
+}
\ No newline at end of file
diff --git a/testinput/glacier/ImmutablePerson.java b/testinput/glacier/ImmutablePerson.java
new file mode 100644
index 0000000..e851d4b
--- /dev/null
+++ b/testinput/glacier/ImmutablePerson.java
@@ -0,0 +1,48 @@
+// @skip-test
+// Does not apply to PICO: shallow immutable support
+
+package glacier;
+
+import qual.Immutable;
+
+import java.util.Date;
+
+/*
+@Immutable class ImmutableDate {
+	double secondsSinceEpoch;
+
+	void setSeconds(double s) {
+		secondsSinceEpoch = s; // Should error!
+	}
+}
+public @Immutable class ImmutablePerson {
+	public ImmutablePerson() {
+		birthdate = new ImmutableDate();
+
+	}
+
+	ImmutableDate birthdate;
+
+	public void test() {
+
+	}
+}
+class Person {
+	String name;
+}
+*/
+
+
+@Immutable public class ImmutablePerson {
+    // Date is mutable
+    // :: error: glacier.mutable.invalid
+    Date birthdate;
+
+    public ImmutablePerson() {
+
+    }
+
+    public void aMethod() {
+
+    }
+}
\ No newline at end of file
diff --git a/testinput/glacier/ImmutablePrimitiveContainer.java b/testinput/glacier/ImmutablePrimitiveContainer.java
new file mode 100644
index 0000000..360fb43
--- /dev/null
+++ b/testinput/glacier/ImmutablePrimitiveContainer.java
@@ -0,0 +1,12 @@
+import qual.Immutable;
+
+@SuppressWarnings("initialization")
+@Immutable
+public class ImmutablePrimitiveContainer {
+    int x;
+
+    public void setX(int x) {
+        // ::error: (illegal.field.write)
+        this.x = x;
+    }
+}
\ No newline at end of file
diff --git a/testinput/glacier/IncorrectUsage.java b/testinput/glacier/IncorrectUsage.java
new file mode 100644
index 0000000..d9624f4
--- /dev/null
+++ b/testinput/glacier/IncorrectUsage.java
@@ -0,0 +1,46 @@
+package glacier;
+
+import qual.*;
+
+@Immutable public class IncorrectUsage {
+    public void okMethod(IncorrectUsage this) {
+
+    }
+
+    public void okMethod2(@Immutable IncorrectUsage this) {
+
+    }
+
+    // PICO Note: adding method.receiver.incompatible
+    // ::error: (type.invalid.annotations.on.use)  ::error: (method.receiver.incompatible)
+    public void badMethod(@Mutable IncorrectUsage this) {
+
+    }
+
+    // ::error: (type.invalid.annotations.on.use)
+    public void badMethod2(@Mutable IncorrectUsage obj) {
+
+    }
+}
+
+
+class IncorrectUsage2 {
+    public void okMethod(IncorrectUsage2 this) {
+
+    }
+
+    public void okMethod2(@Mutable IncorrectUsage2 this) {
+
+    }
+
+    // PICO Note: adding method.receiver.incompatible
+    // ::error: (type.invalid.annotations.on.use)  ::error: (method.receiver.incompatible)
+    public void badMethod(@Immutable IncorrectUsage2 this) {
+
+    }
+
+    // ::error: (type.invalid.annotations.on.use)
+    public void badMethod2(@Immutable IncorrectUsage2 obj) {
+
+    }
+}
\ No newline at end of file
diff --git a/testinput/glacier/IntArgument.java b/testinput/glacier/IntArgument.java
new file mode 100644
index 0000000..b3156ec
--- /dev/null
+++ b/testinput/glacier/IntArgument.java
@@ -0,0 +1,12 @@
+package glacier;
+
+public class IntArgument {
+    public void takeInt(int x) {
+    }
+
+    public void useInt() {
+        for (int i = 0; i < 10; i++) {
+            takeInt(i);
+        }
+    }
+}
\ No newline at end of file
diff --git a/testinput/glacier/IntReturn.java b/testinput/glacier/IntReturn.java
new file mode 100644
index 0000000..e942f3f
--- /dev/null
+++ b/testinput/glacier/IntReturn.java
@@ -0,0 +1,11 @@
+package glacier;
+
+public class IntReturn {
+    public int getInt() {
+        return 42;
+    }
+
+    public void useInt() {
+        int x = getInt();
+    }
+}
\ No newline at end of file
diff --git a/testinput/glacier/IntegerAssignment.java b/testinput/glacier/IntegerAssignment.java
new file mode 100644
index 0000000..681e93f
--- /dev/null
+++ b/testinput/glacier/IntegerAssignment.java
@@ -0,0 +1,11 @@
+package glacier;
+
+public class IntegerAssignment {
+    public Integer getInt() {
+        return 42;
+    }
+
+    public void useInt() {
+        Integer i = getInt();
+    }
+}
\ No newline at end of file
diff --git a/testinput/glacier/InterfaceField.java b/testinput/glacier/InterfaceField.java
new file mode 100644
index 0000000..a9fc1a5
--- /dev/null
+++ b/testinput/glacier/InterfaceField.java
@@ -0,0 +1,14 @@
+// @skip-test
+// Deep immutable
+
+import qual.Immutable;
+
+interface IF_AnInterface {};
+
+@Immutable interface IF_ImmutableInterface extends IF_AnInterface {};
+
+@Immutable public class InterfaceField {
+    // ::error: (glacier.mutable.invalid)
+    IF_AnInterface o;
+    IF_ImmutableInterface o2;
+}
\ No newline at end of file
diff --git a/testinput/glacier/InterfaceSupertype.java b/testinput/glacier/InterfaceSupertype.java
new file mode 100644
index 0000000..1c581d0
--- /dev/null
+++ b/testinput/glacier/InterfaceSupertype.java
@@ -0,0 +1,32 @@
+package glacier;
+
+import qual.Immutable;
+
+interface AnInterface {
+
+}
+
+
+public class InterfaceSupertype {
+
+    public void takeMutable(Object o) {
+
+    }
+
+    public void takeImmutable(Object o) {
+
+    }
+
+    public void doStuff() {
+        AnInterface obj = null;
+
+        takeMutable(obj);
+        takeImmutable(obj);
+    }
+
+    public boolean equals(Object o1,Object o2){
+        if(o1==o2)
+            return true;
+        return o1!=null ? o1.equals(o2) : false;
+    }
+}
\ No newline at end of file
diff --git a/testinput/glacier/InvalidAnnotations.java b/testinput/glacier/InvalidAnnotations.java
new file mode 100644
index 0000000..40574d1
--- /dev/null
+++ b/testinput/glacier/InvalidAnnotations.java
@@ -0,0 +1,12 @@
+// @skip-test
+// who cares bottom
+
+import qual.*;
+
+// ::error: (type.invalid)
+@Bottom class InvalidBottom {};
+
+public class InvalidAnnotations {
+    // ::error: (type.invalid)
+    InvalidBottom b;
+}
\ No newline at end of file
diff --git a/testinput/glacier/InvalidAssignment.java b/testinput/glacier/InvalidAssignment.java
new file mode 100644
index 0000000..26eadf7
--- /dev/null
+++ b/testinput/glacier/InvalidAssignment.java
@@ -0,0 +1,49 @@
+// @skip-test
+// jdk stub difference
+
+package glacier;
+
+import java.util.Calendar;
+
+import qual.Immutable;
+
+
+public @Immutable class InvalidAssignment {
+    class Inner {
+        public int i;
+    }
+
+    String s;
+    // :: error: glacier.mutable.invalid
+    Calendar c;
+    // :: error: glacier.mutable.invalid
+    Inner i;
+    int x;
+
+    public void setString(String s) {
+        // :: error: glacier.assignment
+        this.s = s;
+    }
+
+    public void setX(int x) {
+        // :: error: glacier.assignment
+        this.x = x;
+    }
+
+    public void setMonth(int month) {
+        c.set(Calendar.MONTH, month); // No error here; the problem is that d was mutable in the first place.
+    }
+
+    public void setInner(int i) {
+        this.i.i = i; // No error here; the problem is that this.i was mutable in the first place.
+    }
+}
+
+class AnotherClass {
+    void aMethod() {
+        InvalidAssignment i = new InvalidAssignment();
+
+        // ::error: (glacier.assignment)
+        i.s = "hello";
+    }
+}
\ No newline at end of file
diff --git a/testinput/glacier/InvalidImmutableInterfaceClass.java b/testinput/glacier/InvalidImmutableInterfaceClass.java
new file mode 100644
index 0000000..214c990
--- /dev/null
+++ b/testinput/glacier/InvalidImmutableInterfaceClass.java
@@ -0,0 +1,14 @@
+import qual.Immutable;
+
+import java.lang.Cloneable;
+
+@Immutable interface IIIC_ImmutableInterface {
+}
+
+// The use of IIIC_ImmutableInterface defaulted to @Mutable.
+// So the implement action is valid for the class (implementing a mutable interface)
+// But for the type use of IIIC_ImmutableInterface it is invalid.
+// :: error: type.invalid.annotations.on.use
+public class InvalidImmutableInterfaceClass implements Cloneable, IIIC_ImmutableInterface {
+
+}
\ No newline at end of file
diff --git a/testinput/glacier/InvalidTypeArguments.java b/testinput/glacier/InvalidTypeArguments.java
new file mode 100644
index 0000000..ff89d06
--- /dev/null
+++ b/testinput/glacier/InvalidTypeArguments.java
@@ -0,0 +1,39 @@
+import java.util.Collection;
+import java.util.Collections;
+import java.util.Iterator;
+
+import qual.Immutable;
+import qual.Mutable;
+
+public class InvalidTypeArguments {
+    interface MutableObject {}
+    @Immutable interface ImmutableObject {}
+
+    class Generic<T> {}
+    Generic<MutableObject> mutableObjectGeneric;
+    Generic<ImmutableObject> immutableObjectGeneric;
+
+    class BogusImmutableGeneric<@Immutable T>{}
+    // :: error: (type.argument.type.incompatible)
+    BogusImmutableGeneric<MutableObject> mutableObjectBogusImmutableGeneric;
+    BogusImmutableGeneric<ImmutableObject> immutableObjectBogusImmutableGeneric;
+
+
+    class ImmutableGeneric<@Immutable T extends @Immutable Object>{}
+    // :: error: (type.argument.type.incompatible)
+    ImmutableGeneric<MutableObject> mutableObjectImmutableGeneric;
+    ImmutableGeneric<ImmutableObject> immutableObjectImmutableGeneric;
+
+    class MutableGeneric<@Mutable T>{}
+    MutableGeneric<MutableObject> mutableObjectMutableGeneric;
+    // :: error: (type.argument.type.incompatible)
+    MutableGeneric<ImmutableObject> immutableObjectMutableGeneric;
+
+    public class UnmodifiableCollection {
+        public Iterator<MutableObject> getCellIterator() {
+            Collection<MutableObject> cellCollection = null;
+            Collections.unmodifiableCollection(cellCollection);
+            return Collections.unmodifiableCollection(cellCollection).iterator();
+        }
+    }
+}
\ No newline at end of file
diff --git a/testinput/glacier/MapParameters.java b/testinput/glacier/MapParameters.java
new file mode 100644
index 0000000..57272de
--- /dev/null
+++ b/testinput/glacier/MapParameters.java
@@ -0,0 +1,13 @@
+// @skip-test
+// handling of null
+
+import java.util.Map;
+
+public class MapParameters {
+    public static  void takeMap(Map<String, ? extends Object> m) {};
+
+    public void foo() {
+        Map <String, Integer> m = null;
+        takeMap(m);
+    }
+}
\ No newline at end of file
diff --git a/testinput/glacier/MethodInvocation.java b/testinput/glacier/MethodInvocation.java
new file mode 100644
index 0000000..bc92c5c
--- /dev/null
+++ b/testinput/glacier/MethodInvocation.java
@@ -0,0 +1,14 @@
+package glacier;
+
+import qual.*;
+
+@Immutable interface Interface {
+    public void doStuff();
+}
+
+public class MethodInvocation {
+    public void foo() {
+        Interface i = null;
+        i.doStuff();
+    }
+}
\ No newline at end of file
diff --git a/testinput/glacier/MethodTypeParameters.java b/testinput/glacier/MethodTypeParameters.java
new file mode 100644
index 0000000..d9cf90a
--- /dev/null
+++ b/testinput/glacier/MethodTypeParameters.java
@@ -0,0 +1,7 @@
+import qual.Immutable;
+
+class TypeParameters<E extends @Immutable Object> {
+    static <E> TypeParameters<E> asImmutableList(@Immutable Object[] elements) {
+        return null;
+    }
+}
\ No newline at end of file
diff --git a/testinput/glacier/MutableClassCantHaveImmutableSubclass.java b/testinput/glacier/MutableClassCantHaveImmutableSubclass.java
new file mode 100644
index 0000000..3127882
--- /dev/null
+++ b/testinput/glacier/MutableClassCantHaveImmutableSubclass.java
@@ -0,0 +1,41 @@
+// @skip-test
+//
+
+import qual.Immutable;
+
+
+class Mut {
+    int y = 3;
+}
+
+// ::error: (glacier.nonfinalmember)
+@Immutable class Immut extends Mut { }
+
+class SafeAbstractSuperclass {
+    final int x = 3;
+    final String y = "Hello";
+    final Immut i = null;
+}
+
+@Immutable class Immut2 extends SafeAbstractSuperclass { };
+
+class UnsafeAbstractSuperclass {
+    final int x= 3;
+    String y = "Hello"; // Oops, not final
+    final Immut i = null;
+}
+
+// ::error: (glacier.nonfinalmember)
+@Immutable class Immut3 extends UnsafeAbstractSuperclass { };
+
+
+
+
+class UnsafeAbstractSuperclass2 {
+    final int x = 3;
+    java.util.Date y = null;
+    final Immut i = null;
+}
+
+// ::error: (glacier.nonfinalmember) ::error: (glacier.mutablemember)
+@Immutable class Immut4 extends UnsafeAbstractSuperclass2 { };
\ No newline at end of file
diff --git a/testinput/glacier/NestedGenerics.java b/testinput/glacier/NestedGenerics.java
new file mode 100644
index 0000000..644d95d
--- /dev/null
+++ b/testinput/glacier/NestedGenerics.java
@@ -0,0 +1,21 @@
+import java.util.Iterator;
+
+
+interface Predicate<T> {
+    boolean apply(T var1);
+
+    boolean equals(Object var1);
+}
+
+final class Iterators {
+
+    public static <T> boolean any(Iterator<T> iterator, Predicate<? super T> predicate) {
+        //return indexOf(iterator, predicate) != -1;
+        return true;
+    }
+
+    public static boolean contains(Iterator<?> iterator, Object element) {
+        return any(iterator, null);
+    }
+
+}
\ No newline at end of file
diff --git a/testinput/glacier/NullAssignment.java b/testinput/glacier/NullAssignment.java
new file mode 100644
index 0000000..c799e9e
--- /dev/null
+++ b/testinput/glacier/NullAssignment.java
@@ -0,0 +1,14 @@
+import qual.Immutable;
+
+interface NA_AnInterface {};
+
+
+public class NullAssignment {
+    public void takeObj(Object o) {
+    }
+
+    public void foo() {
+        NA_AnInterface i = null;
+        takeObj(i);
+    }
+}
\ No newline at end of file
diff --git a/testinput/glacier/Override.java b/testinput/glacier/Override.java
new file mode 100644
index 0000000..6328b5a
--- /dev/null
+++ b/testinput/glacier/Override.java
@@ -0,0 +1,18 @@
+package glacier;
+
+import qual.Immutable;
+
+
+@Immutable abstract class Superclass {
+    public abstract void doStuff(int x);
+}
+
+public @Immutable class Override {
+
+
+    public Override() {
+    }
+
+    public void doStuff(int x) {
+    }
+}
\ No newline at end of file
diff --git a/testinput/glacier/PlainObjects.java b/testinput/glacier/PlainObjects.java
new file mode 100644
index 0000000..9b1b1db
--- /dev/null
+++ b/testinput/glacier/PlainObjects.java
@@ -0,0 +1,19 @@
+// @skip-test
+// PICO CAN handle null to @Bottom
+
+import qual.*;
+
+class PlainObjects {
+
+    public void takeObject(Object o) {};
+    public void takeImmutableObject(@Immutable Object o) {};
+
+    void foo () {
+        Object o1 = null;
+        @Immutable Object o2 = null;
+
+        takeObject(o2);
+
+        takeImmutableObject(o1);
+    }
+}
\ No newline at end of file
diff --git a/testinput/glacier/ReadOnlyClass.java b/testinput/glacier/ReadOnlyClass.java
new file mode 100644
index 0000000..8738c71
--- /dev/null
+++ b/testinput/glacier/ReadOnlyClass.java
@@ -0,0 +1,27 @@
+// @skip-test
+
+import qual.*;
+import java.lang.String;
+
+// Classes can't be annotated ReadOnly in their declarations; @Readonly is only for method parameters.
+// ::error: (glacier.readonly.class)
+@Readonly public class ReadOnlyClass {
+}
+
+class ReadOnlyMethodClass {
+    @Readonly ReadOnlyClass roc;
+
+    int @Readonly [] readOnlyIntArray;
+
+    // ::error: (type.invalid.annotations.on.use)
+    void takeReadOnlyString(@Readonly String foo) {}
+    void takeReadOnlyArray(String @Readonly [] foo) {
+        // ::error: (glacier.assignment.array)
+        foo[0] = "Hello, world!";
+    }
+
+    void takeImmutableArray(String @Immutable [] foo) {
+        // ::error: (glacier.assignment.array)
+        foo[0] = "Hello, world!";
+    }
+}
\ No newline at end of file
diff --git a/testinput/glacier/ReadOnlyObject.java b/testinput/glacier/ReadOnlyObject.java
new file mode 100644
index 0000000..bc4c6f3
--- /dev/null
+++ b/testinput/glacier/ReadOnlyObject.java
@@ -0,0 +1,13 @@
+// Reason of Change: defaulting difference.
+
+import qual.*;
+
+public class ReadOnlyObject {
+    // PICO defaults the return type of RDM class to mutable.
+    // But String.valueOf(1) returns immutable.
+    public @Immutable Object foo() {
+        Object cat = null;
+        return true ? String.valueOf(1) : cat;
+    }
+
+}
\ No newline at end of file
diff --git a/testinput/glacier/ResultWrapTest.java b/testinput/glacier/ResultWrapTest.java
new file mode 100644
index 0000000..08809e7
--- /dev/null
+++ b/testinput/glacier/ResultWrapTest.java
@@ -0,0 +1,16 @@
+// @skip-test
+// Guess: in glacter @MaybeMutable is super type of @Immutable. So the use of typevar is allowed.
+
+import qual.Mutable;
+
+public class ResultWrapTest {
+
+    ResultWrapTest() {
+        // while visiting this, the return type must be annotated correctly?
+    }
+
+    static class ResultWrap<T extends @Mutable Object> {
+    }
+
+    final ResultWrap<String> input = null;
+}
\ No newline at end of file
diff --git a/testinput/glacier/StaticAssignment.java b/testinput/glacier/StaticAssignment.java
new file mode 100644
index 0000000..a7bbb8c
--- /dev/null
+++ b/testinput/glacier/StaticAssignment.java
@@ -0,0 +1,22 @@
+// @skip-test
+// !!!!!!!!!!!!!!!
+// GLOBAL is writable in static.
+// removing static will raise error.
+
+import qual.Immutable;
+
+@Immutable
+public class StaticAssignment {
+    public static int GLOBAL = 1; // OK, no error here
+
+    StaticAssignment() {
+        // ::error: (glacier.assignment)
+        GLOBAL = 2;
+    }
+
+    public void setStatics () {
+        // ::error: (glacier.assignment)
+        GLOBAL = 42;
+    }
+
+}
\ No newline at end of file
diff --git a/testinput/glacier/StringTest.java b/testinput/glacier/StringTest.java
new file mode 100644
index 0000000..6f478f3
--- /dev/null
+++ b/testinput/glacier/StringTest.java
@@ -0,0 +1,10 @@
+package glacier;
+
+import qual.Immutable;
+
+import java.lang.String;
+
+@SuppressWarnings("initialization")
+public @Immutable class StringTest {
+    String s; // no error expected here because String should be treated as if it were declared @Immutable.
+}
\ No newline at end of file
diff --git a/testinput/glacier/Subclassing.java b/testinput/glacier/Subclassing.java
new file mode 100644
index 0000000..766b020
--- /dev/null
+++ b/testinput/glacier/Subclassing.java
@@ -0,0 +1,18 @@
+// @skip-test
+// Drop this one: PICO cannot derive from mutable classes
+
+import qual.Immutable;
+
+public class Subclassing { };
+
+class MutSubclass extends Subclassing { };
+
+// OK with the recent change: immutable classes can derive from mutable classes
+@Immutable class InvalidImmutSubclass extends Subclassing { };
+
+
+@Immutable class ImmutableSuper { };
+@Immutable class ImmutableSub extends ImmutableSuper { };
+
+// ::error: (glacier.subclass.mutable)
+class InvalidMutableSub extends ImmutableSuper { };
\ No newline at end of file
diff --git a/testinput/glacier/Transitivity.java b/testinput/glacier/Transitivity.java
new file mode 100644
index 0000000..66f2138
--- /dev/null
+++ b/testinput/glacier/Transitivity.java
@@ -0,0 +1,20 @@
+package glacier;
+
+import qual.Immutable;
+
+@SuppressWarnings("initialization")
+@Immutable class Inner {
+    int x;
+}
+
+@SuppressWarnings("initialization")
+public @Immutable class Transitivity {
+    Inner i;
+
+    public Transitivity() {
+    }
+
+    public void test() {
+
+    }
+}
\ No newline at end of file
diff --git a/testinput/glacier/TransitivityError.java b/testinput/glacier/TransitivityError.java
new file mode 100644
index 0000000..75876f2
--- /dev/null
+++ b/testinput/glacier/TransitivityError.java
@@ -0,0 +1,23 @@
+// @skip-test
+// until the defaulting of fields in immutable class is resolved
+
+package glacier;
+
+import qual.Immutable;
+
+
+class TE_Inner {
+    int x;
+}
+
+public @Immutable class TransitivityError {
+    // :: error: glacier.mutable.invalid
+    TE_Inner i;
+
+    public TransitivityError() {
+    }
+
+    public void test() {
+
+    }
+}
\ No newline at end of file
diff --git a/testinput/glacier/TypeParameter.java b/testinput/glacier/TypeParameter.java
new file mode 100644
index 0000000..a78fdab
--- /dev/null
+++ b/testinput/glacier/TypeParameter.java
@@ -0,0 +1,32 @@
+// @skip-test
+// review glacier's type parameter rule when free
+
+import qual.Immutable;
+
+class E { } // Note same name as type parameter, but mutable class.
+
+@Immutable class TP_Superclass<E> {
+    private E aField; // Should be OK because we'll make sure E is instantiated with an immutable type. This E is the type parameter, not the class above.
+    void aMethod() {
+
+    }
+}
+
+@Immutable public class TypeParameter<E> extends TP_Superclass<E> {
+    private TP_Superclass<? extends E> s;
+    private TP_Superclass<? extends String> t;
+
+    // ::error: (glacier.typeparameter.mutable)
+    private TP_Superclass<? extends java.util.Date> u;
+
+    void aMethod() {
+
+    }
+}
+
+@Immutable class Test {
+    TypeParameter <String> t1 = null; // OK
+
+    // ::error: (glacier.typeparameter.mutable)
+    TypeParameter <java.util.Date> t2 = null;
+}
\ No newline at end of file
diff --git a/testinput/glacier/Unboxing.java b/testinput/glacier/Unboxing.java
new file mode 100644
index 0000000..c614fbd
--- /dev/null
+++ b/testinput/glacier/Unboxing.java
@@ -0,0 +1,8 @@
+public class Unboxing {
+    public void takeNumber(Number n) {};
+
+    public void passDouble() {
+        takeNumber(42.0);
+    }
+
+};
\ No newline at end of file
diff --git a/testinput/glacier/UnmodifiableCollection.java b/testinput/glacier/UnmodifiableCollection.java
new file mode 100644
index 0000000..02138b7
--- /dev/null
+++ b/testinput/glacier/UnmodifiableCollection.java
@@ -0,0 +1,14 @@
+import java.util.Collection;
+import java.util.Collections;
+import java.util.Iterator;
+import java.util.List;
+
+
+interface SCell {};
+
+public class UnmodifiableCollection {
+    public Iterator<SCell> getCellIterator() {
+        Collection<SCell> cellCollection = null;
+        return Collections.unmodifiableCollection(cellCollection).iterator();
+    }
+}
\ No newline at end of file
diff --git a/testinput/glacier/UnmodifiableList.java b/testinput/glacier/UnmodifiableList.java
new file mode 100644
index 0000000..578ef86
--- /dev/null
+++ b/testinput/glacier/UnmodifiableList.java
@@ -0,0 +1,24 @@
+package glacier;
+
+import java.util.List;
+
+
+class ListProcessor {
+    static <T> List<T> process(List<? extends T> c) {
+        // ::warning: [unchecked] unchecked cast
+        return (List<T>)c;
+    }
+}
+
+class AClass {}
+
+public class UnmodifiableList {
+    private List<AClass> _list;
+
+    public void foo() {
+
+        //List<AClass> a = true ? _list : null;
+        List<AClass> l = true ? ListProcessor.process(_list) : _list;
+        //List<AClass> l = ListProcessor.process(_list);
+    }
+}
\ No newline at end of file
diff --git a/testinput/glacier/ValidImmutableInterfaceClass.java b/testinput/glacier/ValidImmutableInterfaceClass.java
new file mode 100644
index 0000000..784f443
--- /dev/null
+++ b/testinput/glacier/ValidImmutableInterfaceClass.java
@@ -0,0 +1,11 @@
+package glacier;
+
+import qual.Immutable;
+
+
+@Immutable interface VIIC_ImmutableInterface {
+}
+
+public @Immutable class ValidImmutableInterfaceClass implements VIIC_ImmutableInterface {
+
+}
\ No newline at end of file
diff --git a/testinput/reiminfer/CFLTests1.java b/testinput/reiminfer/CFLTests1.java
new file mode 100644
index 0000000..c4ce5a2
--- /dev/null
+++ b/testinput/reiminfer/CFLTests1.java
@@ -0,0 +1,50 @@
+
+
+class MyA {
+	String f;
+}
+
+class List{
+    Object[] elems;
+    int count;
+    List() { 
+    	Object[] t = new Object[10];
+        this.elems = t; 
+    }
+    void add(Object m) {
+       Object[] t = this.elems;
+       t[count++] = m;
+    }
+    Object get(int ind) {
+    	Object[] t = this.elems;
+    	Object p = t[ind];
+    	return p;
+    }
+}
+
+class ListClient {
+	List list;
+	ListClient(List l) { 
+		this.list = l; 
+	}
+	Object retrieve() { 
+		List t = this.list;
+		Object r = t.get(0);
+		return r;
+	}
+}
+
+public class CFLTests1 {
+	public static void main(String[] arg) {
+		List l1 = new List();
+		MyA t = new MyA(); 
+		l1.add(t);
+		ListClient client = new ListClient(l1);
+		List l2 = new List();
+		MyA i = new MyA(); i.f = "abc";
+		l2.add(i);
+		MyA s = (MyA) client.retrieve();
+		MyA j = (MyA) l2.get(0);
+		String str = s.f;
+	}
+}
diff --git a/testinput/reiminfer/CFLTests2.java b/testinput/reiminfer/CFLTests2.java
new file mode 100644
index 0000000..4d20033
--- /dev/null
+++ b/testinput/reiminfer/CFLTests2.java
@@ -0,0 +1,18 @@
+class MyB {
+	String f;
+}
+
+public class CFLTests2 {
+	
+	public static MyB id(MyB p) {
+		return p;
+	}
+	
+	public static void main(String[] arg) {
+		MyB b1 = new MyB(); //o1
+		MyB b2 = new MyB(); //o2
+		
+		MyB b3 = id(b1);
+		MyB b4 = id(b2);
+	}	
+}
diff --git a/testinput/reiminfer/CFLTests3.java b/testinput/reiminfer/CFLTests3.java
new file mode 100644
index 0000000..ab1a101
--- /dev/null
+++ b/testinput/reiminfer/CFLTests3.java
@@ -0,0 +1,25 @@
+class Data {
+	String d;
+	public void set(String p) {
+		this.d = p;
+	}
+	
+	public String get() {
+		return this.d;
+	}	
+}
+
+
+public class CFLTests3 {
+	public static void main() {
+		Data data = new Data();
+		String s1 = new String("Ana");
+		data.set(s1);
+		String s2 = data.get();
+		
+		Data data2 = new Data();
+		String s3 = new String("Antun");
+		data2.set(s3);
+		String s4 = data2.get();
+	}
+}
diff --git a/testinput/reiminfer/CFLTests4.java b/testinput/reiminfer/CFLTests4.java
new file mode 100644
index 0000000..7a07a16
--- /dev/null
+++ b/testinput/reiminfer/CFLTests4.java
@@ -0,0 +1,39 @@
+
+public class CFLTests4 {
+	String[] arr1 = new String[10];
+	String[] arr2 = new String[10];
+	/*
+	public CFLTests4() {
+		arr1 = new String[10];
+		arr2 = new String[10];
+	}
+	*/
+	
+	public void putInArr1(String s) {
+		arr1[0] = s;
+	}
+	
+	public void putInArr2(String s) {
+		arr2[0] = s;
+	}
+	
+	public String getFromArr1() {
+		return arr1[0];
+	}
+	
+	public String getFromArr2() {
+		return arr2[0];
+	}
+	
+	public static void main(String[] arg) {
+		CFLTests4 c = new CFLTests4();
+		String s1 = new String("Ana");
+		String s2 = new String("Antun");
+		c.putInArr1(s1);
+		c.putInArr2(s2);
+		
+		String s3 = c.getFromArr1();
+		String s4 = c.getFromArr2();
+		System.out.println(s3+" "+s4);
+	}
+}
diff --git a/testinput/reiminfer/CFLTests5.java b/testinput/reiminfer/CFLTests5.java
new file mode 100644
index 0000000..b74f7f1
--- /dev/null
+++ b/testinput/reiminfer/CFLTests5.java
@@ -0,0 +1,45 @@
+
+public class CFLTests5 {
+	
+	public void putInArr(String s, String[] arr1) {
+		arr1[0] = s;
+	}
+	/*
+	public void putInArr2(String s, String[] arr2) {
+		arr2[0] = s;
+	}
+	*/
+	
+	public String getFromArr(String[] arr1) {
+		return arr1[0];
+	}
+	/*
+	public String getFromArr2(String[] arr2) {
+		return arr2[0];
+	}
+	*/
+	
+	public static void main(String[] arg) {
+		CFLTests5 c = new CFLTests5();
+		String[] arr1 = new String[10];
+		String[] arr2 = new String[10];
+		
+		String s1 = new String("Ana");
+		String s2 = new String("Antun");
+		
+		c.putInArr(s1,arr1);
+		c.putInArr(s2,arr2);
+		
+		String s3 = c.getFromArr(arr1);
+		String s4 = c.getFromArr(arr2);
+		System.out.println(s3+" "+s4);
+		
+		String[] arr3 = new String[10];
+		String s7 = new String("Pooch");
+		arr3[0] = s7; 
+		String s5 = arr3[0];
+		String s6 = s5;
+		
+	}
+}
+	
\ No newline at end of file
diff --git a/testinput/reiminfer/CFLTests6.java b/testinput/reiminfer/CFLTests6.java
new file mode 100644
index 0000000..5f4c65c
--- /dev/null
+++ b/testinput/reiminfer/CFLTests6.java
@@ -0,0 +1,30 @@
+interface I {
+	public void set(String p);
+	public String get();
+}
+
+class IData implements I {
+	String d;
+	public void set(String p) {
+		this.d = p;
+	}
+	
+	public String get() {
+		return this.d;
+	}	
+}
+
+
+public class CFLTests6 {
+	public static void main() {
+		I data = new IData();
+		String s1 = new String("Ana");
+		data.set(s1);
+		String s2 = data.get();
+		
+		I data2 = new IData();
+		String s3 = new String("Antun");
+		data2.set(s3);
+		String s4 = data2.get();
+	}
+}
diff --git a/testinput/reiminfer/CFLTests7.java b/testinput/reiminfer/CFLTests7.java
new file mode 100644
index 0000000..4983976
--- /dev/null
+++ b/testinput/reiminfer/CFLTests7.java
@@ -0,0 +1,30 @@
+class DD {
+	String f;
+}
+
+
+public class CFLTests7 {
+
+	public static DD dd = new DD();
+	
+	public static String theString;
+	
+	public static void main(String[] arg) {
+		String s1 = new String("Ana");
+		String s2 = new String("Antun");
+		
+		theString = s1;
+		dd.f = s2;
+		
+		m();
+		n();		
+	}
+	
+	public static void m() {
+		String s3 = theString;
+	}
+	
+	public static void n() {
+		String s4 = dd.f;
+	}
+}
diff --git a/testinput/reiminfer/CFLTests8.java b/testinput/reiminfer/CFLTests8.java
new file mode 100644
index 0000000..110a0f3
--- /dev/null
+++ b/testinput/reiminfer/CFLTests8.java
@@ -0,0 +1,42 @@
+import java.util.ArrayList;
+import java.util.HashMap;
+
+class MyCrap {
+	int i;
+}
+
+
+public class CFLTests8 {
+	
+	static HashMap<String,MyCrap> hashMap = new HashMap<String,MyCrap>();
+	
+	HashMap<String,MyCrap> map = new HashMap<String,MyCrap>();
+	ArrayList<MyCrap> l = new ArrayList<MyCrap>();
+	
+	public void m() {
+		MyCrap m1 = new MyCrap();
+		MyCrap m2 = new MyCrap();
+		hashMap.put("Ana",m1);
+		
+		map.put("Sweety",m2);
+	}
+	
+	public void n() {
+		MyCrap m3 = hashMap.get("Ana");
+		MyCrap m4 = map.get("Sweety");
+		l.add(m4);
+	}
+	
+	public void o() {
+		MyCrap m5 = l.get(0);
+	}
+	
+	public static void main(String[] args) {
+		CFLTests8 cfl = new CFLTests8();
+		cfl.m();
+		cfl.n();
+		cfl.o();
+	}
+	
+	
+}
diff --git a/testinput/reiminfer/CircularInitialization.java b/testinput/reiminfer/CircularInitialization.java
new file mode 100644
index 0000000..cadcce6
--- /dev/null
+++ b/testinput/reiminfer/CircularInitialization.java
@@ -0,0 +1,35 @@
+class Person {
+	String name;
+	Person partner;
+	
+	public Person(String name) {
+		this.name = name;
+	}
+	
+	public void m(Person p) {
+		this.partner = p;
+	}
+}
+
+class Couple {
+	Person husband;
+	Person wife;
+	public Couple(Person husband, Person wife) {
+		this.husband = husband;
+		this.wife = wife;
+	}
+	public void print() {
+		System.out.println(husband.name+" and "+wife.name);
+	}
+}
+
+public class CircularInitialization {
+	public static void main(String[] args) {
+		Person bob = new Person("Bob");
+		Person sally = new Person("Sally");
+		bob.m(sally);
+		sally.m(bob);
+		Couple c = new Couple(bob,sally);
+		c.print();
+	}
+}
diff --git a/testinput/reiminfer/ImmutableArrays.java b/testinput/reiminfer/ImmutableArrays.java
new file mode 100644
index 0000000..c116d20
--- /dev/null
+++ b/testinput/reiminfer/ImmutableArrays.java
@@ -0,0 +1,38 @@
+public class ImmutableArrays {
+    char[] a;
+    
+	ImmutableArrays() {
+	   a = new char[10];
+	   for (int i=0; i<10; i++) {
+		   a[i] = 'a';
+	   }
+	   //b[0] = 'b';
+	}
+	
+	void m(StringBuffer b) {
+		System.out.println(b.toString());
+		a[0] = 'a';
+		System.out.println(b.toString());
+		b.append("ana"); 
+	}
+	void n() {
+		char[] b = a;
+		b[1] = 'b';
+	}
+	
+	
+	public static void main(String[] args) {
+		char[] bb = new char[100];
+		bb[5] = 'a';
+		ImmutableArrays i = new ImmutableArrays();
+		i.m(new StringBuffer("Boza"));
+		i.n();
+		if (i.a[1] == 'b')
+			System.out.println("AHA");
+		else
+			System.out.println("A-NO");
+		// i.a[2] = 'c';
+		StringBuffer b = new StringBuffer("Ana");		
+		System.out.println(i.a[1]+i.a[0]);
+	}
+}
diff --git a/testinput/reiminfer/InitMethod.java b/testinput/reiminfer/InitMethod.java
new file mode 100644
index 0000000..36c4a48
--- /dev/null
+++ b/testinput/reiminfer/InitMethod.java
@@ -0,0 +1,30 @@
+class A {
+	char[] arr;
+	public A() {
+		arr = new char[10];
+		arr[0] = 'a';
+		init("Ana");
+	}
+	
+	void init(String arg) {
+		System.out.println(arg);
+		for (int i=0; i<10; i++) {
+			System.out.println(arr[i]);
+			//arr[i] = 'b';
+		}
+		//m(arr);
+	}
+	
+	void m(char[] b) {
+		b[0]='a';
+	}
+	
+}
+
+public class InitMethod {
+	public static void main(String[] arg) {
+		A a = new A();
+		a.init("Ana");
+		//a.m(a.arr);
+	}
+}
diff --git a/testinput/reiminfer/Library.java b/testinput/reiminfer/Library.java
new file mode 100644
index 0000000..e6bf73d
--- /dev/null
+++ b/testinput/reiminfer/Library.java
@@ -0,0 +1,16 @@
+import java.util.*;
+
+public class Library {
+
+    public void foo() {
+        Set<X> set = new HashSet<X>();
+        X a1 = new X();
+        set.add(a1);
+        Set<X> set2 = set;
+        int size = set2.size();
+    }
+}
+
+class X {
+    String f;
+}
diff --git a/testinput/reiminfer/LibraryUse.java b/testinput/reiminfer/LibraryUse.java
new file mode 100644
index 0000000..13ac96a
--- /dev/null
+++ b/testinput/reiminfer/LibraryUse.java
@@ -0,0 +1,12 @@
+import java.util.*;
+
+public class LibraryUse {
+	public static void main(String[] arg) {
+		ArrayList<String> al = new ArrayList<String>();
+		al.add("Boza");
+		al.add("Katarina");
+		ArrayList<String> al1 = al;
+		int i = al1.size();
+		System.out.println(i);
+	}
+}
diff --git a/testinput/reiminfer/Test1.java b/testinput/reiminfer/Test1.java
new file mode 100644
index 0000000..8a2b224
--- /dev/null
+++ b/testinput/reiminfer/Test1.java
@@ -0,0 +1,44 @@
+
+class B {
+	protected StringBuffer name;
+	
+	public B(StringBuffer s) {
+		name = s;
+	}
+}
+
+class C extends B {
+	
+	public C() {
+		super(new StringBuffer("Ana"));
+	}	
+	
+	public void set() {
+		name.append("Boza");
+	}
+	public String get() {
+		return name.toString();
+	}
+}
+
+class D {
+	C c = new C();
+	public void m() {
+		c.set();
+	}
+	
+	public String n() {
+		return c.get();
+	}
+}
+
+public class Test1 {
+	
+	public static void main(String[] arg) {
+		D d = new D();
+		d.m();
+		d.n();
+		
+	}
+	
+}
diff --git a/testinput/reiminfer/Test2.java b/testinput/reiminfer/Test2.java
new file mode 100644
index 0000000..393aa07
--- /dev/null
+++ b/testinput/reiminfer/Test2.java
@@ -0,0 +1,21 @@
+
+public class Test2 {
+
+	public static char[] copy(char[] a) {
+		char[] r = new char[a.length];
+		for (int i=0; i < a.length; i++) {
+			r[i] = a[i];
+		}
+		return r;
+	}
+	
+	public static void main(String[] argc) {
+		char[] a = new char[5];
+		for (int i=0; i<5; i++)
+			a[i] = 'a';
+		char[] r = copy(a);
+		// System.out.println(r);
+		//r[0] = 'a';
+	}
+	
+}
diff --git a/testinput/reiminfer/Test3.java b/testinput/reiminfer/Test3.java
new file mode 100644
index 0000000..4ec7b0a
--- /dev/null
+++ b/testinput/reiminfer/Test3.java
@@ -0,0 +1,40 @@
+class F {
+	char[] arr;
+}
+
+class E {
+	
+	char[] arr;
+	void m() {
+		arr = new char[5];
+		for (int i=0; i<5; i++) {
+			arr[i] = 10;
+		}
+	}
+	char[] n() {
+		return arr;
+	}
+	void o(F p) {
+		p.arr = arr;
+	}
+}
+
+
+public class Test3 {
+	public static E create() {
+		E e = new E();
+		e.m();
+		return e;
+	}
+  public static void main(String[] argc) {
+	  E d = create();
+	  // E d = new E();
+	  // d.m();
+	  // char[] b = d.n();
+	  F f = new F();
+	  d.o(f);
+	  char[] b = f.arr;
+	  b[0] = 'a';
+	  System.out.println(b[0]);
+  }
+}
diff --git a/testinput/reiminfer/Test4.java b/testinput/reiminfer/Test4.java
new file mode 100644
index 0000000..d708cbb
--- /dev/null
+++ b/testinput/reiminfer/Test4.java
@@ -0,0 +1,50 @@
+class BB {
+	int i;
+}
+
+class AA {
+	char[] arr;
+	BB f;
+	AA() {
+		arr = new char[2];
+		f = new BB();
+	}
+	
+	BB get() { return f; }
+	
+	char[] getArray() { return arr; }
+	
+	static AA createInstance() {
+		return new AA();
+	}
+	
+	
+ }
+
+
+public class Test4 {
+	
+	BB f;
+	
+	BB m() {
+		AA a = AA.createInstance();
+		BB bb = a.get();
+		f = bb;
+		return bb;
+	}
+	
+	void n() {
+		f.i = 0;
+	}
+	
+	static Test4 create() {
+		return new Test4();
+	}
+	
+	public static void main(String[] arg) {
+		Test4 t = create();
+		BB bb = t.m();
+		t.n();
+		// bb.i = 0;
+	}
+}
diff --git a/testinput/reiminfer/TheClass.java b/testinput/reiminfer/TheClass.java
new file mode 100644
index 0000000..8863c93
--- /dev/null
+++ b/testinput/reiminfer/TheClass.java
@@ -0,0 +1,72 @@
+import qual.*;
+
+public class TheClass {
+    public @PolyMutable String f;
+    public static String sf;
+    public Object of = null;
+    public static int sof = 1;
+
+//    public TheClass() {
+//        f = "hello";
+//    }
+
+//    public TheClass(String p1) {
+//        this.f = p1;
+//    }
+
+    public String doSomethingElse(
+            @PolyMutable TheClass this,
+            String p1, 
+            Object p2,
+            int p4) {
+        String s1 = p1;
+        String s2 = s1;
+        String s3 = s2 + " world";
+        return s3;
+    }
+
+    public String doSomething(@Readonly TheClass this){
+        String s = doSomethingElse(f, null, 1);
+        return s;
+    }
+
+//    public String doMore() {
+//        String d1 = "hello";
+//        TheClass c = new TheClass();
+//        f = d1;
+//        c.f = d1;
+//        TheClass c2 = new TheClass();
+//        c = c2;
+//        return c.f;
+//    }
+
+//    public String toString() {
+//        return f;
+//    }
+
+//    public boolean equals(Object o) {
+//        return true;
+//    }
+}
+
+class AnotherClass extends TheClass {
+
+
+//    @Override
+//    public void doSomething(){
+//        String[] localA2 = testArrays2();
+//        String[] localA3 = localA2;
+//    }
+
+
+//    String[] fieldA;
+//
+//    public void testArrays() {
+//        String[] localA = this.fieldA;
+//    }
+
+//    public String[] testArrays2() {
+//        return fieldA;
+//    }
+
+}
diff --git a/testinput/reiminfer/ThisLeak.java b/testinput/reiminfer/ThisLeak.java
new file mode 100644
index 0000000..38fdebd
--- /dev/null
+++ b/testinput/reiminfer/ThisLeak.java
@@ -0,0 +1,26 @@
+class AAA {
+	ThisLeak f;
+}
+
+public class ThisLeak {
+   private ThisLeak f;
+   
+   public void m() {
+	   this.f = this;
+	   System.out.println("Tests leak into field of this");
+   }
+   
+   public void n(AAA a) {
+	   a.f = this;
+	   System.out.println("Tests leak into field of parameter");
+   }
+   
+   public static void main(String[] arg) {
+	   ThisLeak tl = new ThisLeak();
+	   AAA aaa = new AAA();
+	   tl.m();
+	   tl.n(aaa);
+	   
+   }
+   
+}
diff --git a/testinput/reiminfer/ThisLeak2.java b/testinput/reiminfer/ThisLeak2.java
new file mode 100644
index 0000000..f33defb
--- /dev/null
+++ b/testinput/reiminfer/ThisLeak2.java
@@ -0,0 +1,20 @@
+class Helper {
+	ThisLeak2 f;
+}
+
+public class ThisLeak2 {
+	public void m(Helper h) {
+		n(h);
+	}
+	public void n(Helper h) {
+		ThisLeak2[] arr = new ThisLeak2[1];
+		arr[0] = this;
+		// h.f = this;
+	}
+	
+	public static void main(String[] arg) {
+		ThisLeak2 tl2 = new ThisLeak2();
+		Helper h = new Helper();
+		tl2.m(h);
+	}
+}
diff --git a/testinput/reiminfer/ThisLeak3.java b/testinput/reiminfer/ThisLeak3.java
new file mode 100644
index 0000000..4312529
--- /dev/null
+++ b/testinput/reiminfer/ThisLeak3.java
@@ -0,0 +1,18 @@
+class ZZZ {
+	ThisLeak3 f;
+}
+public class ThisLeak3 {
+	void m(ZZZ z, ThisLeak3 p) {
+		z.f = p;
+	}
+	
+	void n(ZZZ z) {
+		m(z,this);
+	}
+	
+	public static void main(String[] arg) {
+		ThisLeak3 tl3 = new ThisLeak3();
+		ZZZ z = new ZZZ();
+		tl3.n(z);
+	}
+}
diff --git a/testinput/reiminfer/ThisLeak4.java b/testinput/reiminfer/ThisLeak4.java
new file mode 100644
index 0000000..8149c5e
--- /dev/null
+++ b/testinput/reiminfer/ThisLeak4.java
@@ -0,0 +1,24 @@
+public class ThisLeak4 {
+
+	public void n() {
+		System.out.println("This is n");
+	}
+	
+	public void o() {
+		innerClass ic = new innerClass();
+		ic.m();
+	}
+	
+	public static void main(String[] arg) {
+		ThisLeak4 tl4 = new ThisLeak4();
+		tl4.o();
+	}
+	
+	public class innerClass {
+		int f;
+		public void m() {
+			System.out.println("Boza");
+			n();
+		}
+	}
+}
diff --git a/testinput/reiminfer/ThisLeak5.java b/testinput/reiminfer/ThisLeak5.java
new file mode 100644
index 0000000..bc01b4d
--- /dev/null
+++ b/testinput/reiminfer/ThisLeak5.java
@@ -0,0 +1,21 @@
+class Boza {
+	ThisLeak5 f;
+	int y;
+}
+public class ThisLeak5 {
+	int x;
+	Boza b;
+	
+	public ThisLeak5() {
+		ThisLeak5 p = this;
+		
+		p.b = new Boza();
+		p.x = 0;
+		
+		int y = p.x;
+		Boza bb = p.b;
+		this.b = bb;
+		this.x = y;
+	}
+	
+}
diff --git a/testinput/reiminfer/ThisLeak6.java b/testinput/reiminfer/ThisLeak6.java
new file mode 100644
index 0000000..588e8fe
--- /dev/null
+++ b/testinput/reiminfer/ThisLeak6.java
@@ -0,0 +1,22 @@
+class YYY {
+	ThisLeak6 f;
+}
+
+public class ThisLeak6 {
+	int x;
+	
+	public ThisLeak6 id() {
+		return this;
+	}
+	
+	public void m() {
+		System.out.println("fjdfkjd");
+		ThisLeak6 tl6 = id();
+		tl6.x = 0;
+	}
+	
+	public void n(YYY y) {
+		y.f = id();
+	}
+	
+}