diff --git a/abstract-semantics.txt b/abstract-semantics.txt
new file mode 100644
index 0000000..ae4b6a5
--- /dev/null
+++ b/abstract-semantics.txt
@@ -0,0 +1,277 @@
+/* ============  Selector Functions ============ */
+
+/*  === General Infrastructure === */
+sel pcs: unit -> [int]; // gives all pcs of the contract
+sel pcsForOpcode: int -> [int]; // gives all pcs for a certain opcode
+sel argumentForPc: int -> [int]; // gives the argument for the opcode at pc (can only be invoked pcs containing a PUSH, JUMP or JUMPI)
+
+/* ============ Opcodes ============= */
+
+const ADD := 0;
+const AND := 1;
+const LE := 2;
+const PUSH := 3;
+const POP := 4; 
+const MLOAD := 5;
+const MSTORE := 6;
+const SLOAD := 7;
+const SSTORE := 8;
+const TIMESTAMP := 9; 
+const BALANCE := 10;
+const INPUT := 11;
+const ADDRESS := 12;
+const GAS := 13;
+const JUMP := 14; 
+const JUMPI := 15;
+const RETURN := 16;
+const STOP := 17;
+const FAIL := 18;
+const CALL := 19; 
+
+/* ============  Abstract Domain and abstract operations ============ */
+
+eqtype AbsDom := @T | @V<int>; /* Abstract Domain: @T represents the top element, V(v) concrete elements of value v */
+
+// operation that checks whether a value is concrete (not top)
+op isConcrete(a:AbsDom): bool := match a with | @T => false | _ => true;  
+
+//operation that extracts the concrete value from an abstract value (in case of @T it defaults to 0)
+op extractConcrete(a:AbsDom): int := match a with | @V(x) => x | _ => 0;
+
+op isAbstract(a:AbsDom): bool := ~ isConcrete(a);
+
+op absAdd(a:AbsDom, b:AbsDom): AbsDom :=
+	match (a, b) with
+	| (@V(n), @V(m)) => @V(n+m)
+	| _ => @T;
+
+op absAnd(a:AbsDom, b:AbsDom): AbsDom :=
+	match (a, b) with
+	| (@V(n), @V(m)) => (n > 0 && m > 0) ? (@V(1)) : (@V(0))
+	| _ => @T;
+
+op absLe(a:AbsDom, b:AbsDom): AbsDom :=
+	match (a, b) with
+	| (@V(n), @V(m)) => (n <= m) ? (@V(1)) : (@V(0))
+	| _ => @T;
+
+/* ============  Predicates ============ */
+
+pred ExState{int}: int * array<AbsDom> * array<AbsDom> * AbsDom * array<AbsDom> * bool; // Execution State: <pc>, size, stack, memory, input, storage, cl (call level)
+pred Exc{}: bool; // Exceptional Halting: cl, predicate signalizing exceptional halting
+pred Halt{}: array<AbsDom> * AbsDom * bool; // Successful Halting: storage, return value, cl
+
+
+/* ============  Abstract Rules ============ */
+
+rule exception :=
+	for (!pc: int) in pcs()
+	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
+		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl)
+		=> Exc(?cl);
+
+rule add :=
+	for (!pc: int) in pcsForOpcode(ADD)
+	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?x: AbsDom, ?y: AbsDom]
+		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
+		?size > 1,
+		?x = select ?sa (?size - 1),
+		?y = select ?sa (?size - 2)
+		=> ExState{!pc+1}(?size - 1, store ?sa (?size - 2) (absAdd(?x, ?y)), ?mem, ?in, ?stor, ?cl);
+
+rule and :=
+	for (!pc: int) in pcsForOpcode(AND)
+	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?x: AbsDom, ?y: AbsDom]
+		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
+		?size > 1,
+		?x = select ?sa (?size - 1),
+		?y = select ?sa (?size - 2)
+		=> ExState{!pc+1}(?size - 1, store ?sa (?size - 2) (absAnd(?x, ?y)), ?mem, ?in, ?stor, ?cl);
+
+rule le :=
+	for (!pc: int) in pcsForOpcode(LE)
+	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?x: AbsDom, ?y: AbsDom]
+		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
+		?size > 1,
+		?x = select ?sa (?size - 1),
+		?y = select ?sa (?size - 2)
+		=> ExState{!pc+1}(?size - 1, store ?sa (?size - 2) (absLe(?x, ?y)), ?mem, ?in, ?stor, ?cl);
+
+rule push :=
+	for (!pc: int) in pcsForOpcode(PUSH), (!v: int) in argumentForPc(!pc)
+	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
+		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl)
+		=> ExState{!pc+1}(?size + 1, store ?sa ?size @V(!v), ?mem, ?in, ?stor, ?cl);
+
+rule pop :=
+	for (!pc: int) in pcsForOpcode(POP)
+	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
+		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
+		?size >= 1
+		=> ExState{!pc+1}(?size - 1, ?sa, ?mem, ?in, ?stor, ?cl);
+
+rule mstore :=
+	for (!pc: int) in pcsForOpcode(MSTORE)
+	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?p: AbsDom, ?v: AbsDom]
+		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
+		?size >= 2,
+		?p = select ?sa (?size - 1),
+		isConcrete(?p),
+		?v = select ?sa (?size - 2)
+		=> ExState{!pc+1}(?size - 2, ?sa, store ?mem extractConcrete(?p) ?v, ?in, ?stor, ?cl),
+    	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?p: AbsDom, ?v: AbsDom]
+		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
+		?size >= 2,
+		?p = select ?sa (?size - 1),
+		isAbstract(?p)
+		=> ExState{!pc+1}(?size - 2, ?sa, [@T], ?in, ?stor, ?cl);
+
+rule mload :=
+	for (!pc: int) in pcsForOpcode(MLOAD)
+    	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?p: AbsDom, ?v: AbsDom]
+		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
+		?size >= 1,
+		?p = select ?sa (?size -1),
+		isConcrete(?p),
+		?v = select ?mem (extractConcrete(?p))
+		=> ExState{!pc+1}(?size, store ?sa (?size - 1) ?v, ?mem, ?in, ?stor, ?cl),
+	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?p: AbsDom, ?v: AbsDom]
+		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
+		?size >= 1,
+		?p = select ?sa (?size -1),
+		isAbstract(?p)
+		=> ExState{!pc+1}(?size, store ?sa (?size - 1) @T, ?mem, ?in, ?stor, ?cl);
+
+rule sload :=
+	for (!pc: int) in pcsForOpcode(SLOAD)
+	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?v: AbsDom, ?p: AbsDom]
+		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
+		?size >= 1,
+		?p = select ?sa (?size -1),
+		isConcrete(?p),
+		?v = select ?stor extractConcrete(?p)
+		=> ExState{!pc+1}(?size, store ?sa (?size - 1) ?v, ?mem, ?in, ?stor, ?cl),
+	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?p: AbsDom]
+		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
+		?size >= 1,
+		?p = select ?sa (?size -1),
+		isAbstract(?p)
+		=> ExState{!pc+1}(?size, store ?sa (?size - 1) @T, ?mem, ?in, ?stor, ?cl);
+
+rule sstore :=
+	for (!pc: int) in pcsForOpcode(SSTORE)
+	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?p: AbsDom, ?v: AbsDom]
+		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
+		?size >= 2,
+		?p = select ?sa (?size -1),
+		isConcrete(?p),
+		?v = select ?sa (?size -2)
+		=> ExState{!pc+1}(?size - 2, ?sa, ?mem, ?in, store ?stor extractConcrete(?p) ?v, ?cl),
+	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?p: AbsDom]
+		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
+		?size >= 2,
+		?p = select ?sa (?size -1),
+		isAbstract(?p)
+		=> ExState{!pc+1}(?size - 2, ?sa, ?mem, ?in, [@T], ?cl);
+
+rule timestamp :=
+	for (!pc: int) in pcsForOpcode(TIMESTAMP)
+	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
+		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl)
+		=> ExState{!pc+1}(?size + 1, store ?sa ?size @T, ?mem, ?in, ?stor, ?cl);
+
+rule balance :=
+	for (!pc: int) in pcsForOpcode(BALANCE)
+	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
+		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
+		?size >= 1
+		=> ExState{!pc+1}(?size, store ?sa (?size - 1) @T, ?mem, ?in, ?stor, ?cl);
+
+rule input :=
+	for (!pc: int) in pcsForOpcode(INPUT)
+	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
+		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl)
+		=> ExState{!pc+1}(?size + 1, store ?sa ?size ?in, ?mem, ?in, ?stor, ?cl);
+
+rule address :=
+	for (!pc: int) in pcsForOpcode(ADDRESS)
+	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
+		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl)
+		=> ExState{!pc+1}(?size + 1, store ?sa ?size @T, ?mem, ?in, ?stor, ?cl);
+
+rule gas :=
+	for (!pc: int) in pcsForOpcode(GAS)
+	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
+		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl)
+		=> ExState{!pc+1}(?size + 1, store ?sa ?size @T, ?mem, ?in, ?stor, ?cl);
+
+rule jump :=
+	for (!pc: int) in pcsForOpcode(JUMP), (!j: int) in argumentForPc(!pc)
+	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
+		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl)
+		=> ExState{!j}(?size, ?sa, ?mem, ?in, ?stor, ?cl);
+
+rule jumpi :=
+	for (!pc: int) in pcsForOpcode(JUMPI), (!j: int) in argumentForPc(!pc)
+	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?p: AbsDom]
+		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
+		?size >= 1,
+		?p = select ?sa (?size - 1),
+		(isAbstract(?p) || extractConcrete(?p) != 0)
+		=> ExState{!j}(?size-1, ?sa, ?mem, ?in, ?stor, ?cl),
+    	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?p: AbsDom]
+		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
+		?size >= 1,
+		?p = select ?sa (?size - 1),
+		(isAbstract(?p) || extractConcrete(?p) = 0)
+		=> ExState{!pc+1}(?size-1, ?sa, ?mem, ?in, ?stor, ?cl);
+
+rule return :=
+	for (!pc: int) in pcsForOpcode(RETURN)
+	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?p: AbsDom]
+		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
+		?size >= 1,
+		?p = select ?sa (?size -1)
+		=> Halt{}(?stor, ?p, ?cl);
+
+rule stop :=
+	for (!pc: int) in pcsForOpcode(STOP)
+	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
+		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl)
+		=> Halt{}(?stor, @V(0), ?cl);
+
+rule fail :=
+	for (!pc: int) in pcsForOpcode(FAIL)
+	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
+		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl)
+		=> Exc(?cl);
+
+rule call1 :=
+	for (!pc: int) in pcsForOpcode(CALL)
+	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
+		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
+		?size > 3
+		=> ExState{0}(0, [@V(0)], [@V(0)], @T, ?stor, true);
+
+rule call2 :=
+	for (!pc: int) in pcsForOpcode(CALL)
+	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?storInv:array<AbsDom>, ?r: AbsDom]
+		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
+		?size > 3,
+		Halt{}(?storInv, ?r, true)
+		=> ExState{0}(0, [@V(0)], [@V(0)], @T, ?storInv, true);
+
+rule call3 :=
+	for (!pc: int) in pcsForOpcode(CALL)
+	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
+		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
+		?size > 3
+		=> ExState{!pc+1}(?size-3, store ?sa (?size - 4) @T, [@T], ?in, [@T], ?cl);
+
+/* ============  Initialization ============ */
+
+rule initOp :=
+	clause
+		true 
+		=> ExState{0}(0, [@V(0)], [@V(0)], @T, [@T], false); // execution starts at pc 0 in empty execution state
+
diff --git a/alice.txt b/alice.txt
new file mode 100644
index 0000000..4a90b09
--- /dev/null
+++ b/alice.txt
@@ -0,0 +1,14 @@
+PUSH 4294967295;
+SLOAD; 
+PUSH 1;
+LE;
+PUSH 64;
+JUMPI 13;
+PUSH 0;
+PUSH 2;
+INPUT;
+CALL;
+PUSH 1;
+PUSH 4294967295;
+SSTORE;
+STOP;
diff --git a/bob.txt b/bob.txt
new file mode 100644
index 0000000..b980c8b
--- /dev/null
+++ b/bob.txt
@@ -0,0 +1,14 @@
+PUSH 4294967295;
+SLOAD;
+PUSH 1;
+LE;
+JUMPI 13;
+PUSH 64;
+PUSH 0;
+PUSH 2;
+INPUT;
+CALL;
+PUSH 1;
+PUSH 4294967295;
+SSTORE;
+STOP;
diff --git a/call-contract.txt b/call-contract.txt
new file mode 100644
index 0000000..f9658f0
--- /dev/null
+++ b/call-contract.txt
@@ -0,0 +1,15 @@
+// writes 10 to 3 in storage
+/* 0 */ PUSH 10; 
+/* 1 */ PUSH 3; 
+/* 2 */ SSTORE;
+// calls another contract
+/* 3 */ PUSH 0;		// oa
+/* 4 */ PUSH 2; 	// id
+/* 5 */ PUSH 3; 	// va
+/* 6 */ PUSH 42; 	// to
+/* 7 */ CALL; 
+// writes 20 to 3 in storage
+/* 8 */ PUSH 20;
+/* 9 */ PUSH 3;
+/* 10 */ SSTORE; 
+/* 11 */ STOP;
\ No newline at end of file
diff --git a/call-tests.txt b/call-tests.txt
new file mode 100644
index 0000000..993db19
--- /dev/null
+++ b/call-tests.txt
@@ -0,0 +1,120 @@
+/* Special tests for the Call rules. To be run with call-contract.txt */
+
+// Check that the storage can have the right values before calling (at this point there is only one possible value at call level 0)
+test storageSoundnesBeforeTest expect SAT 
+	[?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
+		ExState{7}(4, ?sa, ?mem, ?in, ?stor, false),
+		stackMoreAbstractThanForall{4}(?sa, store (store (store (store [@V(0)] 0 @V(0)) 1 @V(2)) 2 @V(3)) 3 @V(42)),
+		arrayMoreAbstractThan{1}(?mem, store [UPDATEDUMMY] 0 @UP(0, @V(0))),
+		arrayMoreAbstractThan{1}(?stor, store [UPDATEDUMMY] 0 @UP(3, @V(10))); 
+
+test storagePrecisePossibleBeforeTest expect SAT 
+	[?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
+		ExState{7}(4, ?sa, ?mem, ?in, ?stor, false),
+		stackEqualForall{4}(?sa, store (store (store (store [@V(0)] 0 @V(0)) 1 @V(2)) 2 @V(3)) 3 @V(42)),
+		?mem = [@V(0)],
+		(select ?stor 3) = @V(10);  
+
+test storagePreciseUniqueBeforeTest expect UNSAT 
+	[?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
+		ExState{7}(?size, ?sa, ?mem, ?in, ?stor, false),
+		(?size != 4 || ?mem != [@V(0)] 
+		|| stackInequalExists{4}(?sa, store (store (store (store [@V(0)] 0 @V(0)) 1 @V(2)) 2 @V(3)) 3 @V(42)) 
+		|| (select ?stor 3) != @V(10)); 
+
+//Check for the right storage when reentering (can be 10 or 20, but nothing else)
+test storageSoundnessReenteringTest1 expect SAT 
+	[?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
+		ExState{0}(0, ?sa, ?mem, ?in, ?stor, true),
+		valueMoreAbstractThan(?in, @T),
+		arrayMoreAbstractThan{1}(?mem, store [UPDATEDUMMY] 0 @UP(0, @V(0))), 
+		arrayMoreAbstractThan{1}(?stor, store [UPDATEDUMMY] 0 @UP(3, @V(10))); 
+
+test storageSoundnessReenteringTest2 expect SAT 
+	[?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
+		ExState{0}(0, ?sa, ?mem, ?in, ?stor, true),
+		valueMoreAbstractThan(?in, @T),
+		arrayMoreAbstractThan{1}(?mem, store [UPDATEDUMMY] 0 @UP(0, @V(0))), 
+		arrayMoreAbstractThan{1}(?stor, store [UPDATEDUMMY] 0 @UP(3, @V(20))); 
+
+test storagePrecisePossibleReenteringTest1 expect SAT 
+	[?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
+		ExState{0}(0, ?sa, ?mem, ?in, ?stor, true),
+		?mem = [@V(0)], 
+		?in = @T, 
+		(select ?stor 3) = @V(10);  
+
+test storagePrecisePossibleReenteringTest2 expect SAT 
+	[?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
+		ExState{0}(0, ?sa, ?mem, ?in, ?stor, true),
+		?mem = [@V(0)],
+		?in = @T,
+		(select ?stor 3) = @V(20); 
+
+test storagePreciseUniqueReenteringTest expect UNSAT 
+	[?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
+		ExState{0}(?size, ?sa, ?mem, ?in, ?stor, true),
+		(?mem != [@V(0)] || ?in != @T || ?size != 0 || 
+		(select ?stor 3) != @V(10) && (select ?stor 3) != @V(20)); 
+
+// Check that the storage is sound after reentering (on both levels)
+test storageSoundnessResumeTest1 expect SAT 
+	[?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
+		ExState{8}(1, ?sa, ?mem, ?in, ?stor, false),
+		stackMoreAbstractThanForall{1}(?sa, store [@V(0)] 0 @T),
+		arrayMoreAbstractThan{1}(?mem, store [UPDATEDUMMY] 0 @UP(0, @T)), 
+		arrayMoreAbstractThan{1}(?stor, store [UPDATEDUMMY] 0 @UP(3, @V(10))); 
+
+test storageSoundnessResumeTest2 expect SAT 
+	[?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
+		ExState{8}(1, ?sa, ?mem, ?in, ?stor, false),
+		stackMoreAbstractThanForall{1}(?sa, store [@V(0)] 0 @T),
+		arrayMoreAbstractThan{1}(?mem, store [UPDATEDUMMY] 0 @UP(0, @T)), 
+		arrayMoreAbstractThan{1}(?stor, store [UPDATEDUMMY] 0 @UP(3, @V(20))); 
+
+test storageSoundnessResumeTest3 expect SAT 
+	[?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
+		ExState{8}(1, ?sa, ?mem, ?in, ?stor, true),
+		stackMoreAbstractThanForall{1}(?sa, store [@V(0)] 0 @T),
+		arrayMoreAbstractThan{1}(?mem, store [UPDATEDUMMY] 0 @UP(0, @T)), 
+		arrayMoreAbstractThan{1}(?stor, store [UPDATEDUMMY] 0 @UP(3, @V(10))); 
+
+test storageSoundnessResumeTest4 expect SAT 
+	[?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
+		ExState{8}(1, ?sa, ?mem, ?in, ?stor, true),
+		stackMoreAbstractThanForall{1}(?sa, store [@V(0)] 0 @T),
+		arrayMoreAbstractThan{1}(?mem, store [UPDATEDUMMY] 0 @UP(0, @T)), 
+		arrayMoreAbstractThan{1}(?stor, store [UPDATEDUMMY] 0 @UP(3, @V(20))); 
+
+// Check that the storage is right when halting
+test storageSoundnessHaltTest1 expect SAT 
+	[?res: AbsDom, ?stor: array<AbsDom>]
+	Halt(?stor, ?res, false), 
+	valueMoreAbstractThan(?res, @V(0)),
+	arrayMoreAbstractThan{1}(?stor, store [UPDATEDUMMY] 0 @UP(3, @V(20)));
+
+test storageSoundnessHaltTest2 expect SAT 
+	[?res: AbsDom, ?stor: array<AbsDom>]
+	Halt(?stor, ?res, true),
+	valueMoreAbstractThan(?res, @V(0)), 
+	arrayMoreAbstractThan{1}(?stor, store [UPDATEDUMMY] 0 @UP(3, @V(20)));
+
+test storagePrecisePossibleHaltTest1 expect SAT 
+	[?res: AbsDom, ?stor: array<AbsDom>]
+	Halt(?stor, ?res, false),
+	?res = @V(0), 
+	(select ?stor 3) = @V(20);
+
+test storagePrecisePossibleHaltTest2 expect SAT 
+	[?res: AbsDom, ?stor: array<AbsDom>]
+	Halt(?stor, ?res, true),
+	?res = @V(0),  
+	(select ?stor 3) = @V(20);
+
+test storagePreciseUniqueHaltTest expect UNSAT 
+	[?res: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
+	Halt(?stor, ?res, ?cl), 
+	(select ?stor 3) != @V(20) || (?res != @V(0)) ;
+
+
+
diff --git a/call1.txt b/call1.txt
new file mode 100644
index 0000000..b9063cb
--- /dev/null
+++ b/call1.txt
@@ -0,0 +1,33 @@
+rule rule1 :=
+    for (!pc: int) in pcsForOpcode(CALL)
+	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
+		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
+		?size > 3
+		=> ExState{0}(0, [@V(0)], [@V(0)], @T, ?stor, true);
+
+rule rule2 :=
+	for (!pc: int) in pcsForOpcode(CALL)
+	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?storInv: array<AbsDom>, ?r: AbsDom]
+		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
+		?size > 3,
+		Halt{}(?storInv,?r,true)
+		=> ExState{0}(0, [@V(0)], [@V(0)], @T, ?storInv, true);
+
+rule rule3 :=
+	for (!pc: int) in pcsForOpcode(CALL)
+	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
+		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
+		?size > 3,
+		isAbstract(select ?sa (?size - 4))
+		=> ExState{!pc+1}(?size-3, store ?sa (?size - 4) @T, [@T], ?in, [@T], ?cl);
+
+rule rule4 :=
+	for (!pc: int) in pcsForOpcode(CALL)
+	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?p: AbsDom, ?storInv: array<AbsDom>, ?r: AbsDom]
+        	ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
+		?size > 3,
+		?p = select ?sa (?size - 4),
+		isConcrete(?p),
+		extractConcrete(?p) >= 0,
+		Halt(?storInv, ?r, true)
+		=> ExState{!pc+1}(?size-3, store ?sa (?size - 4) @T, store ?mem (extractConcrete (?p)) ?r, ?in, [@T], ?cl);
diff --git a/call2.txt b/call2.txt
new file mode 100644
index 0000000..f646356
--- /dev/null
+++ b/call2.txt
@@ -0,0 +1,29 @@
+rule rule1 :=
+	for (!pc: int) in pcsForOpcode(CALL)
+	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
+		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
+		?size > 3
+		=> ExState{0}(0, [@V(0)], [@V(0)], @T, ?stor, true);
+
+rule rule2 :=
+	for (!pc: int) in pcsForOpcode(CALL)
+	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?storInv: array<AbsDom>, ?r: AbsDom]
+		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
+		?size > 3,
+			Halt{}(?storInv, ?r, true)
+		=> ExState{0}(0, [@V(0)], [@V(0)], @T, ?storInv, true);
+
+rule rule3 :=
+	for (!pc: int) in pcsForOpcode(CALL)
+	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
+		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
+		?size > 3
+		=> ExState{!pc+1}(?size-3, store ?sa (?size - 4) @T, [@T], ?in, ?stor, ?cl);
+
+rule rule4 :=
+	for (!pc: int) in pcsForOpcode(CALL)
+	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?storInv: array<AbsDom>, ?r: AbsDom]
+		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
+		?size > 3,
+		Halt(?storInv, ?r, true)
+		=> ExState{!pc+1}(?size-3, store ?sa (?size - 4) @T, [@T], ?in, ?storInv, ?cl);
diff --git a/call3.txt b/call3.txt
new file mode 100644
index 0000000..a0c8ad7
--- /dev/null
+++ b/call3.txt
@@ -0,0 +1,13 @@
+rule rule1 :=
+	for (!pc: int) in pcsForOpcode(CALL)
+	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
+		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
+		?size > 3
+		=> ExState{0}(0, [@V(0)], [@V(0)], @T, ?stor, true);
+
+rule rule2 :=
+	for (!pc: int) in pcsForOpcode(CALL)
+	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
+		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
+		?size > 3
+		=> ExState{!pc+1}(?size-3, store ?sa (?size - 4) @T, [@T], ?in, [@T], ?cl);
diff --git a/call4.txt b/call4.txt
new file mode 100644
index 0000000..24f0c7e
--- /dev/null
+++ b/call4.txt
@@ -0,0 +1,22 @@
+rule rule1 :=
+	for (!pc: int) in pcsForOpcode(CALL)
+	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?v: AbsDom]
+		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
+		?size > 3,
+		?v = select ?sa (?size -3)
+		=> ExState{0}(0, [@V(0)], [@V(0)], ?v, ?stor, true);
+
+rule rule2 :=
+	for (!pc: int) in pcsForOpcode(CALL)
+    	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?storInv: array<AbsDom>, ?r: AbsDom]
+		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
+		?size > 3,
+		Halt{}(?storInv, ?r, true)
+		=> ExState{0}(0, [@V(0)], [@V(0)], @T, ?storInv, true);
+
+rule rule3 :=
+	for (!pc: int) in pcsForOpcode(CALL)
+	clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
+		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
+		?size > 3
+		=> ExState{!pc+1}(?size-3, store ?sa (?size - 4) @T, [@T], ?in, [@T], ?cl);
diff --git a/call5.txt b/call5.txt
new file mode 100644
index 0000000..475f31a
--- /dev/null
+++ b/call5.txt
@@ -0,0 +1,28 @@
+rule rule1 :=
+    for (!pc: int) in pcsForOpcode(CALL)
+    clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
+        ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
+        ?size > 3
+        => ExState{0}(0, [@V(0)], [@V(0)], @T, ?stor, true);
+
+rule rule2 :=
+    for (!pc: int) in pcsForOpcode(CALL)
+    clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?storInv: array<AbsDom>, ?r: AbsDom]
+        ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
+        ?size > 3,
+        Halt{}(?storInv, ?r, true)
+        => ExState{0}(0, [@V(0)], [@V(0)], @T, ?storInv, true);
+
+rule rule3 :=
+    for (!pc: int) in pcsForOpcode(CALL)
+    clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
+        ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
+        ?size > 3
+        => ExState{!pc+1}(?size-3, store ?sa (?size - 4) @V(1), [@T], ?in, [@T], ?cl);
+
+rule rule4 :=
+    for (!pc: int) in pcsForOpcode(CALL)
+    clause [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
+        ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
+        ?size > 3
+        => ExState{!pc+1}(?size-3, store ?sa (?size - 4) @V(0), ?mem, ?in, [@T], ?cl);
diff --git a/counter-example1.txt b/counter-example1.txt
new file mode 100644
index 0000000..fdc005c
--- /dev/null
+++ b/counter-example1.txt
@@ -0,0 +1,23 @@
+PUSH 123; // address of sent
+SLOAD; // get value of sent
+PUSH 1;
+LE; // check 1 <= sent (= !(sent < 1))
+JUMPI 22;
+PUSH 1;
+PUSH 123;
+SSTORE; // sent = 1
+PUSH ~1337; // - oa
+PUSH 0; // - id
+PUSH 2; // - va
+INPUT; // - to
+CALL; // call 1
+PUSH ~1337;
+MLOAD;
+PUSH 123;
+SSTORE; // sent = memory[oa]
+PUSH ~1337;
+PUSH 0; // - id
+PUSH 2; // - va
+INPUT; // - to
+CALL; // call 2
+STOP;
diff --git a/counter-example3.txt b/counter-example3.txt
new file mode 100644
index 0000000..4c589f3
--- /dev/null
+++ b/counter-example3.txt
@@ -0,0 +1,20 @@
+INPUT;
+JUMPI 16;
+PUSH 2;
+SLOAD;
+PUSH 1;
+LE; // 1 <= sent ( == !(sent < 1))
+JUMPI 19;
+PUSH 1;
+PUSH 2;
+SSTORE; // sent := 1
+PUSH 1;
+PUSH 2;
+PUSH 2;
+PUSH 4;
+CALL;
+STOP;
+PUSH 0;
+PUSH 2;
+SSTORE; // sent := 0
+STOP;
diff --git a/counter-example4.txt b/counter-example4.txt
new file mode 100644
index 0000000..a80a533
--- /dev/null
+++ b/counter-example4.txt
@@ -0,0 +1,11 @@
+PUSH 0;
+INPUT;
+LE; // x <= 0
+JUMPI 10;
+PUSH 123; // - oa
+PUSH 0; // - id, important
+PUSH 2; // - va
+PUSH 1337; // - to, attacker
+CALL;
+STOP;
+FAIL;
diff --git a/local-contract.txt b/local-contract.txt
new file mode 100644
index 0000000..06d3f1a
--- /dev/null
+++ b/local-contract.txt
@@ -0,0 +1,54 @@
+/* 0 */ PUSH 1; 			// [1]
+/* 1 */ PUSH ~2; 			// [~2, 1]
+/* 2 */ ADD; 				// [~1]
+/* 3 */ PUSH 1;				// [1, ~1]
+/* 4 */ AND;				// [0]
+/* 5 */ PUSH 2;				// [2, 0]
+/* 6 */ LE;					// [0]
+/* 7 */ PUSH ~1; 			// [~1, 0]
+/* 8 */ LE;					// [1]
+/* 9 */ PUSH 336633572;		// [336633572, 1]
+/* 10 */ AND;				// [1]
+/* 11 */ POP; 				// []
+/* 12 */ PUSH 246435;		// [246435]
+/* 13 */ MLOAD;				// [0]
+/* 14 */ PUSH 2; 			// [2, 0]
+/* 15 */ ADD; 				// [2]
+/* 16 */ PUSH 1;			// [1, 2]
+/* 17 */ MSTORE;			// [] 				[[1 -> 2]]
+/* 18 */ PUSH 1; 			// [1]				
+/* 19 */ MLOAD; 			// [2]
+/* 20 */ TIMESTAMP; 		// [T, 2]
+/* 21 */ MLOAD;				// [T, 2]
+/* 22 */ MSTORE; 			// []				[[_ -> T]]
+/* 23 */ PUSH ~42;			// [~42]
+/* 24 */ SLOAD;				// [T]
+/* 25 */ SLOAD;				// [T]
+/* 26 */ POP;				// []
+/* 27 */ PUSH ~1337;		// [~1337]
+/* 28 */ PUSH ~67;			// [~67, ~1337]
+/* 29 */ SSTORE;			// []									((~67 -> ~1337))
+/* 30 */ PUSH ~67;			// [~67]
+/* 31 */ SLOAD;				// [~1337]
+/* 32 */ BALANCE; 			// [T]
+/* 33 */ SLOAD;				// [T]
+/* 34 */ INPUT;				// [T, T]
+/* 35 */ SSTORE;			// []									((_ -> T))
+/* 36 */ ADDRESS; 			// [T]
+/* 37 */ GAS;				// [T, T]
+/* 38 */ JUMP 40;			// [T, T]
+/* 39 */ RETURN; 			// UNREACHABLE (over-jumped)
+/* 40 */ JUMPI 43; 			// [T] 
+/* 41 */ BALANCE;			// [T]
+/* 42 */ RETURN; 			// [T]
+/* 43 */ JUMPI 45; 			// []
+/* 44 */ STOP; 				// []
+/* 45 */ GAS; 				// [T]
+/* 46 */ JUMPI 48;			// []
+/* 47 */ FAIL;				//
+/* 48 */ PUSH 1;			// [1]
+/* 49 */ JUMPI 51;			// []
+/* 50 */ FAIL; 				// UNREACHABLE (over-jumped)
+/* 51 */ STOP; 				// []
+// CALL tests are missing
+
diff --git a/local-tests.txt b/local-tests.txt
new file mode 100644
index 0000000..e9cbe2b
--- /dev/null
+++ b/local-tests.txt
@@ -0,0 +1,289 @@
+/* Tests for the local instructions of tinyEVM. To be run on local-contract.txt */
+
+op pcToConfig(pc: int): Config := 
+	match pc with
+	| 0 => @C(	0, 
+				[@V(0)], 
+				UPDATELISTDUMMY,  
+				UPDATELISTDUMMY)
+	| 1 => @C(	1, 
+				store [@V(0)] 0 @V(1), 
+				UPDATELISTDUMMY, 
+				UPDATELISTDUMMY)
+	| 2 => @C(	2, 
+				store (store [@V(0)] 0 @V(1)) 1 @V(~2), 
+				UPDATELISTDUMMY,
+				UPDATELISTDUMMY)
+	| 3 => @C(	1, 
+				store [@V(0)] 0 @V(~1),
+				UPDATELISTDUMMY, 
+				UPDATELISTDUMMY)
+	| 4 => @C(	2, 
+				store (store [@V(0)] 0 @V(~1)) 1 @V(1),
+				UPDATELISTDUMMY, 
+				UPDATELISTDUMMY)
+	| 5 => @C(	1, 
+				store [@V(0)] 0 @V(0),
+				UPDATELISTDUMMY, 
+				UPDATELISTDUMMY)
+	| 6 => @C(	2, 
+				store (store [@V(0)] 0 @V(0)) 1 @V(2),
+				UPDATELISTDUMMY, 
+				UPDATELISTDUMMY)
+	| 7 => @C(	1, 
+				store [@V(0)] 0 @V(0),
+				UPDATELISTDUMMY, 
+				UPDATELISTDUMMY)
+	| 8 => @C(	2, 
+				store (store [@V(0)] 0 @V(0)) 1 @V(~1),
+				UPDATELISTDUMMY, 
+				UPDATELISTDUMMY)
+	| 9 => @C(	1, 
+				store [@V(0)] 0 @V(1),
+				UPDATELISTDUMMY, 
+				UPDATELISTDUMMY)
+	| 10 => @C(	2, 
+				store (store [@V(0)] 0 @V(1)) 1 @V(336633572),
+				UPDATELISTDUMMY, 
+				UPDATELISTDUMMY)
+	| 11 => @C(	1, 
+				store [@V(0)] 0 @V(1),
+				UPDATELISTDUMMY, 
+				UPDATELISTDUMMY)
+	| 12 => @C(	0, 
+				[@V(0)],
+				UPDATELISTDUMMY, 
+				UPDATELISTDUMMY)
+	| 13 => @C(	1, 
+				store [@V(0)] 0 @V(246435),
+				UPDATELISTDUMMY, 
+				UPDATELISTDUMMY)
+	| 14 => @C(	1, 
+				[@V(0)],
+				UPDATELISTDUMMY, 
+				UPDATELISTDUMMY)
+	| 15 => @C(	2, 
+				store [@V(0)] 1 @V(2),
+				UPDATELISTDUMMY, 
+				UPDATELISTDUMMY)
+	| 16 => @C(	1, 
+				store [@V(0)] 0 @V(2),
+				UPDATELISTDUMMY, 
+				UPDATELISTDUMMY)
+	| 17 => @C(	2, 
+				store (store [@V(0)] 0 @V(2)) 1 @V(1),
+				UPDATELISTDUMMY, 
+				UPDATELISTDUMMY)
+	| 18 => @C(	0, 
+				[@V(0)],
+				addUpdate(UPDATELISTDUMMY, @UP(1, @V(2))),
+				UPDATELISTDUMMY)
+	| 19 => @C(	1, 
+				store [@V(0)] 0 @V(1),
+				addUpdate(UPDATELISTDUMMY, @UP(1, @V(2))),
+				UPDATELISTDUMMY)
+	| 20 => @C(	1, 
+				store [@V(0)] 0 @V(2),
+				addUpdate(UPDATELISTDUMMY, @UP(1, @V(2))),
+				UPDATELISTDUMMY)
+	| 21 => @C(	2, 
+				store (store [@V(0)] 0 @V(2)) 1 @T,
+				addUpdate(UPDATELISTDUMMY, @UP(1, @V(2))),
+				UPDATELISTDUMMY)
+	| 22 => @C(	2, 
+				store (store [@V(0)] 0 @V(2)) 1 @T,
+				addUpdate(UPDATELISTDUMMY, @UP(1, @V(2))),
+				UPDATELISTDUMMY)
+	| 23 => @C(	0, 
+				[@V(0)],
+				addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
+				UPDATELISTDUMMY)
+	| 24 => @C(	1, 
+				store [@V(0)] 0 @V(~42),
+				addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
+				UPDATELISTDUMMY)
+	| 25 => @C(	1, 
+				store [@V(0)] 0 @T,
+				addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
+				UPDATELISTDUMMY)
+	| 26 => @C(	1, 
+				store [@V(0)] 0 @T,
+				addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
+				UPDATELISTDUMMY)
+	| 27 => @C(	0, 
+				[@V(0)],
+				addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
+				UPDATELISTDUMMY)
+	| 28 => @C(	1, 
+				store [@V(0)] 0 @V(~1337),
+				addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
+				UPDATELISTDUMMY)
+	| 29 => @C(	2, 
+				store (store [@V(0)] 0 @V(~1337)) 1 @V(~67),
+				addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
+				UPDATELISTDUMMY)
+	| 30 => @C(	0, 
+				[@V(0)],
+				addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
+				addUpdate(UPDATELISTDUMMY, @UP(~67, @V(~1337))))
+	| 31 => @C(	1, 
+				store [@V(0)] 0 @V(~67),
+				addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
+				addUpdate(UPDATELISTDUMMY, @UP(~67, @V(~1337))))
+	| 32 => @C(	1, 
+				store [@V(0)] 0 @V(~1337),
+				addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
+				addUpdate(UPDATELISTDUMMY, @UP(~67, @V(~1337))))
+	| 33 => @C(	1, 
+				store [@V(0)] 0 @T,
+				addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
+				addUpdate(UPDATELISTDUMMY, @UP(~67, @V(~1337))))
+	| 34 => @C(	1, 
+				store [@V(0)] 0 @T,
+				addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
+				addUpdate(UPDATELISTDUMMY, @UP(~67, @V(~1337))))
+	| 35 => @C(	2, 
+				store (store [@V(0)] 0 @T) 1 @T,
+				addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
+				addUpdate(UPDATELISTDUMMY, @UP(~67, @V(~1337))))
+	| 36 => @C(	0, 
+				[@V(0)],
+				addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
+				addUpdate(UPDATELISTDUMMY, @UP(~67, @T)))
+	| 37 => @C(	1, 
+				store [@V(0)] 0 @T,
+				addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
+				addUpdate(UPDATELISTDUMMY, @UP(~67, @T)))
+	| 38 => @C(	2, 
+				store (store [@V(0)] 0 @T) 1 @T,
+				addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
+				addUpdate(UPDATELISTDUMMY, @UP(~67, @T)))
+	| 40 => @C(	2, 
+				store (store [@V(0)] 0 @T) 1 @T,
+				addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
+				addUpdate(UPDATELISTDUMMY, @UP(~67, @T)))
+	| 41 => @C(	1, 
+				store [@V(0)] 0 @T,
+				addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
+				addUpdate(UPDATELISTDUMMY, @UP(~67, @T)))
+	| 42 => @C(	1, 
+				store [@V(0)] 0 @T,
+				addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
+				addUpdate(UPDATELISTDUMMY, @UP(~67, @T)))
+	| 43 => @C(	1, 
+				store [@V(0)] 0 @T,
+				addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
+				addUpdate(UPDATELISTDUMMY, @UP(~67, @T)))
+	| 44 => @C(	0, 
+				[@V(0)],
+				addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
+				addUpdate(UPDATELISTDUMMY, @UP(~67, @T)))
+	| 45 => @C(	0, 
+				[@V(0)],
+				addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
+				addUpdate(UPDATELISTDUMMY, @UP(~67, @T)))
+	| 46 => @C(	1, 
+				store [@V(0)] 0 @T,
+				addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
+				addUpdate(UPDATELISTDUMMY, @UP(~67, @T)))
+	| 47 => @C(	0, 
+				[@V(0)],
+				addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
+				addUpdate(UPDATELISTDUMMY, @UP(~67, @T)))
+	| 48 => @C(	0, 
+				[@V(0)],
+				addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
+				addUpdate(UPDATELISTDUMMY, @UP(~67, @T)))
+	| 49 => @C(	1, 
+				store [@V(0)] 0 @V(1),
+				addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
+				addUpdate(UPDATELISTDUMMY, @UP(~67, @T)))
+	| 51 => @C(	0, 
+				[@V(0)],
+				addUpdate(UPDATELISTDUMMY, @UP(1, @T)),
+				addUpdate(UPDATELISTDUMMY, @UP(~67, @T)))
+	| _ => @C(	0, 
+				[@V(0)], 
+				UPDATELISTDUMMY, 
+				UPDATELISTDUMMY);
+
+const INTERVALS := 3; 
+
+test pcToStackTest expect SAT [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
+	ExState{1}(?size, ?sa, ?mem, ?in, ?stor, ?cl),
+	(@V(1)) = (select (getStackArray(pcToConfig(1))) 0);
+
+
+test soundnessTest expect SAT 
+	for (!i: int) in interval(0, INTERVALS), (!pc: int) in interval((!i = 0)? (0): ((!i = 1)?(40):(51)), (!i = 0)? (39): ((!i = 1)?(50):(52))) // ugly way to only invoke the rule on certain intervals
+	[?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
+		ExState{!pc}(getStackSize(pcToConfig(!pc)), ?sa, ?mem, @T, ?stor, false),
+		stackMoreAbstractThanForall{getStackSize(pcToConfig(!pc))}(?sa, getStackArray(pcToConfig(!pc))),
+		arrayMoreAbstractThan{getUpdateSize(getMemUpdateList(pcToConfig(!pc)))}(?mem, getUpdates(getMemUpdateList(pcToConfig(!pc)))),
+		arrayMoreAbstractThan{getUpdateSize(getStorUpdateList(pcToConfig(!pc)))}(?stor, getUpdates(getStorUpdateList(pcToConfig(!pc))))
+		;
+
+test precisionPossibleTest expect SAT
+ 	for (!i: int) in interval(0, INTERVALS), (!pc: int) in interval((!i = 0)? (0): ((!i = 1)?(40):(51)), (!i = 0)? (39): ((!i = 1)?(50):(52)))
+	[?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
+		ExState{!pc}(getStackSize(pcToConfig(!pc)), ?sa, ?mem, @T, ?stor, false),
+		stackEqualForall{getStackSize(pcToConfig(!pc))}(?sa, getStackArray(pcToConfig(!pc))),
+		arrayEqual{getUpdateSize(getMemUpdateList(pcToConfig(!pc)))}(?mem, getUpdates(getMemUpdateList(pcToConfig(!pc)))),
+		arrayEqual{getUpdateSize(getStorUpdateList(pcToConfig(!pc)))}(?stor, getUpdates(getStorUpdateList(pcToConfig(!pc))))
+		;
+
+test precisionUniqueTest expect UNSAT
+	for (!i: int) in interval(0, INTERVALS), (!pc: int) in interval((!i = 0)? (0): ((!i = 1)?(40):(51)), (!i = 0)? (39): ((!i = 1)?(50):(52)))
+	[?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
+		ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, false),
+		(?size != getStackSize(pcToConfig(!pc))) 
+		|| (stackInequalExists{getStackSize(pcToConfig(!pc))}(?sa, getStackArray(pcToConfig(!pc)))) 
+		|| (arrayInequalExists{getUpdateSize(getMemUpdateList(pcToConfig(!pc)))}(?mem, getUpdates(getMemUpdateList(pcToConfig(!pc)))))
+		|| (?in != @T) 
+		|| (arrayInequalExists{getUpdateSize(getStorUpdateList(pcToConfig(!pc)))}(?stor, getUpdates(getStorUpdateList(pcToConfig(!pc)))))
+		;
+
+
+/* Additional Tests concerning reachability, halting, etc. */
+
+// pcs 39 and 50 should be unreachable because they are over-jumped
+test unreachable39Test expect UNSAT
+		[?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
+		ExState{39}(?size, ?sa, ?mem, ?in, ?stor, ?cl);
+
+test unreachable50Test expect UNSAT
+		[?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool]
+		ExState{50}(?size, ?sa, ?mem, ?in, ?stor, ?cl);
+
+// Tests for correct halting
+test haltSoundnessTest expect SAT
+	[?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?res: AbsDom]
+	Halt(?stor, ?res, false),
+	valueMoreAbstractThan(?res, @V(0)); 
+
+test haltPrecisePossibleTest expect SAT
+	[?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?res: AbsDom]
+	Halt(?stor, @V(0), false);
+
+// the only possible return results are 0 and T (due to stop and RETURN)
+test haltPreciionUniquenessTest expect UNSAT
+	[?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?res: AbsDom]
+	Halt(?stor, ?res, false),
+	(?res != @V(0) && ?res != @T); 
+
+// Reaching an exceptional state should be possible
+test exceptionPossibleTest expect SAT
+	Exc(false);
+
+test noCallTest2 expect UNSAT
+	Exc(true);
+
+
+/*
+query testQuery [?size: int, ?sa: array<AbsDom>, ?mem: array<AbsDom>,?in: AbsDom, ?stor: array<AbsDom>, ?cl: bool, ?res: AbsDom, ?p: AbsDom]
+	ExState{13}(?size, ?sa, ?mem, ?in, ?stor, ?cl), ?size > 0, 
+		?p = select ?sa (?size -1),
+		?res = (isConcrete(?p))? (select ?mem (extractConcrete(?p))):(@T), 
+		?res = @V(0); */
+
+
diff --git a/queries.txt b/queries.txt
new file mode 100644
index 0000000..e47f784
--- /dev/null
+++ b/queries.txt
@@ -0,0 +1,7 @@
+/* ============  Reentrancy query ============ */
+
+query reentrancyCall for (!pc:int) in pcsForOpcode(CALL) 
+	[?sa: array<AbsDom>, ?mem: array<AbsDom>, ?in: AbsDom, ?stor: array<AbsDom>, ?size:int] 
+	ExState{!pc}(?size, ?sa, ?mem, ?in, ?stor, true);
+
+
diff --git a/report/report.pdf b/report/report.pdf
new file mode 100644
index 0000000..7dbc7e0
Binary files /dev/null and b/report/report.pdf differ
diff --git a/report/report.tex b/report/report.tex
index 5c0ca34..bb31522 100644
--- a/report/report.tex
+++ b/report/report.tex
@@ -17,9 +17,9 @@
 
 % please enter your group number your names and matriculation numbers here
 %TODO
-\newcommand{\groupnumber}{Our group number}
-\newcommand{\name}{Our names}
-\newcommand{\matriculation}{Our matriculations, same order as the names}
+\newcommand{\groupnumber}{5}
+\newcommand{\name}{Tobias Eidelpes}
+\newcommand{\matriculation}{01527193}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %           End of customization         %
@@ -31,7 +31,7 @@
 \setlength{\headsep}{20pt}
 \setlength{\textheight}{680pt}
 \pagestyle{fancy}
-\fancyhf{} 
+\fancyhf{}
 \fancyhead[L]{Formal Methods for Security and Privacy \projnumber\ - minnieThor}
 \fancyhead[C]{}
 \fancyhead[R]{Group \groupnumber}
@@ -43,7 +43,7 @@
 \thispagestyle{empty}
 \noindent\framebox[\linewidth]{%
  \begin{minipage}{\linewidth}%
- \hspace*{5pt} \textbf{Formal Methods for Security and Privacy (SS2020)} \hfill Prof.~Matteo Maffei \hspace*{5pt}\\
+ \hspace*{5pt} \textbf{Formal Methods for Security and Privacy (SS2021)} \hfill Prof.~Matteo Maffei \hspace*{5pt}\\
 
  \begin{center}
   {\bf\Large Project \projnumber~-- \Title}
@@ -65,21 +65,52 @@ Our group consists of the following members:
 \end{center}
 
 \section{Abstract Semantics}
-\emph{Nothing to fill in here, unless you feel that there is something about the implementation that we should consider when grading.}
+\emph{Nothing to fill in here, unless you feel that there is something about the
+implementation that we should consider when grading.}
 
 \section{Fixing reentrancy}
 
-\paragraph{Justification for the soundness of \texttt{alice.txt}:} 
+\subsubsection*{Justification for the soundness of \texttt{alice.txt}:}
 
-  %TODO
-  
- \section{Soundness of the \texttt{CALL} rules}
- 
- \paragraph{Soundness classification of \texttt{CALL} rule sets:}
- 
- \paragraph{Intuition for the sound rule sets:}
- 
- \paragraph{Attack descriptions for the counter examples to the unsound rule sets:}
+By switching the order of line 5 and line 6 in \texttt{alice.txt}, the contract
+\texttt{bob.txt} has been fixed. This works because \texttt{sent} is set to 1
+\emph{before} the call instruction is executed and therefore reentering the
+function is possible but will not execute another call instruction because
+\texttt{sent} has already been set to 1. The contract now follows the
+\emph{Check-Effects-Interactions Pattern}, which requires that checks and state
+changes have to occur before calls to other contracts.
+
+\section{Soundness of the \texttt{CALL} rules}
+
+\subsubsection*{Soundness classification of \texttt{CALL} rule sets:}
+
+\textbf{Call 1}: Unsound \\
+\textbf{Call 2}: Sound \\
+\textbf{Call 3}: Unsound \\
+\textbf{Call 4}: Unsound \\
+\textbf{Call 5}: Sound
+
+\subsubsection*{Intuition for the sound rule sets:}
+
+\paragraph{Call 2:}
+
+The first two rules are the same rules as presented in the lecture. The third rule
+models the case where the contract resumes execution after a call with the same
+storage as before the call. This rule applies when the contract was not called
+and produced a successful halting state before the contract resumes the
+execution after the call.
+
+The fourth rule, however, models the case where the contract resumes execution
+after it was left by another call from a contract that resulted in a halting
+state.
+
+\paragraph{Call 5:}
+
+As for Call 2, the first two rules are the same as presented in the lecture. The
+third rule is correct because in case of $sa[size - 4] = 1$, the local memory
+and the persistent storage are correctly over-approximated. The other case is
+where $sa[size - 4] = 0$. In this case the caller's memory may not be
+manipulated, as formalized by the small-step semantics.
 
 \end{document}
 
diff --git a/test-infrastructure.txt b/test-infrastructure.txt
new file mode 100644
index 0000000..2cf5b9e
--- /dev/null
+++ b/test-infrastructure.txt
@@ -0,0 +1,90 @@
+/* Testing infrastructure */ 
+
+sel interval: int * int -> [int]; // interval function: interval (m, n) provides the numbers m, ..., n-1
+
+op valueMoreAbstractThan (a: AbsDom, b:AbsDom): bool :=
+	match (a, b) with 
+	| (@T, _) => true
+	| (@V(x), @V(y)) => x = y
+	| _ => false; 
+
+// Checks whether there exists a position where the two stacks disagree
+op stackInequalExists{!size: int}(sa: array<AbsDom>, sb: array<AbsDom>): bool := 
+	for (!i: int) in interval(0,!size): || ((select sa !i) != (select sb !i));
+
+// Checks whether the stacks agree at all positions
+op stackEqualForall{!size: int}(sa: array<AbsDom>, sb: array<AbsDom>): bool := 
+	for (!i: int) in interval(0,!size): && ((select sa !i) = (select sb !i));
+
+// Checks that the first stack is more abstract than the second one at all positions
+op stackMoreAbstractThanForall{!size: int}(sa: array<AbsDom>, sb: array<AbsDom>): bool := 
+	for (!i: int) in interval(0,!size): && (valueMoreAbstractThan(select sa !i, select sb !i));
+
+// Update representation for AbsDom arrays. Used for easily checking against a sequence of probing points in memory or storage
+datatype Update := @UP<int*AbsDom>; 
+datatype UpdateList := @UPLIST<int*array<Update>>;
+
+const UPDATEDUMMY := @UP(0, @T);
+const UPDATELISTDUMMY := @UPLIST(0, [UPDATEDUMMY]);
+
+op addUpdate(updates: UpdateList, up: Update): UpdateList := 
+	match updates with 
+	| @UPLIST(size,  ups) => @UPLIST(size + 1, store ups size up)
+	| _ => UPDATELISTDUMMY;
+
+// Checks whether the array sa agrees with all updates of the Update array sb
+op arrayEqual{!size:int} (sa: array<AbsDom>, sb: array<Update>): bool := 
+	for (!i:int) in interval(0, !size): &&
+		(match (select sb !i) with 
+		| @UP(p, v) => (select sa p) = v
+		| _ => false)
+	;
+
+// Checks whether the array sa is at all update points more concrete than the updates in sb
+op arrayMoreAbstractThan{!size:int} (sa: array<AbsDom>, sb: array<Update>): bool := 
+	for (!i:int) in interval(0, !size): &&
+		(match (select sb !i) with 
+		| @UP(p, v) => valueMoreAbstractThan(select sa p, v)
+		| _ => false)
+	;
+
+// Checks whether array sa disagrees on one of the  update points with the updates in sb
+op arrayInequalExists{!size:int} (sa: array<AbsDom>, sb: array<Update>): bool := 
+	for (!i:int) in interval(0, !size): ||
+		(match (select sb !i) with 
+		| @UP(p, v) => (select sa p) != v
+		| _ => false)
+	;
+
+// Configurations that we use for testing. Consist of the stack size, the stack array, and update lists for memory and storage (to probe at the specified points)
+datatype Config := @C<int*array<AbsDom>*UpdateList*UpdateList>;
+
+op getStackSize(conf: Config): int := 
+	match conf with
+	| @C(size, sa, mem, stor) => size
+	| _ => 0;
+
+op getStackArray(conf: Config): array<AbsDom> := 
+	match conf with
+	| @C(size, sa, mem, stor) => sa
+	| _ => [@T];
+
+op getMemUpdateList(conf: Config): UpdateList := 
+	match conf with
+	| @C(size, sa, mem, stor) => mem
+	| _ => UPDATELISTDUMMY;
+
+op getStorUpdateList(conf: Config): UpdateList := 
+	match conf with
+	| @C(size, sa, mem, stor) => stor
+	| _ => UPDATELISTDUMMY;
+
+op getUpdateSize(ul: UpdateList): int := 
+	match ul with 
+	| @UPLIST(s, ua) => s
+	| _ => 0;
+
+op getUpdates(ul: UpdateList): array<Update> := 
+	match ul with
+	| @UPLIST(s, ua) => ua
+	| _ => [UPDATEDUMMY];
\ No newline at end of file