diff --git a/examples/a.out b/examples/a.out
new file mode 100755
index 0000000000000000000000000000000000000000..81e51b36cd97f40e411fa57ab58a740248bba2d7
Binary files /dev/null and b/examples/a.out differ
diff --git a/examples/get_sign.bc b/examples/get_sign.bc
new file mode 100644
index 0000000000000000000000000000000000000000..9b6d64807d3f7ca6e46b8102c0a0b438e2bc07a6
Binary files /dev/null and b/examples/get_sign.bc differ
diff --git a/examples/get_sign.c b/examples/get_sign.c
index 2cf595996551871852cc969b39850317b6f5173c..fb9195fd8100a2140c9d89ee04372b09f0d12ef8 100644
--- a/examples/get_sign.c
+++ b/examples/get_sign.c
@@ -31,12 +31,20 @@ int main()
// > klee get_sign.bc
//
// [your answer here]
+// KLEE: Using Z3 solver backend
+//
+// KLEE: done: total instructions = 31
+// KLEE: done: completed paths = 3
+// KLEE: done: generated tests = 3
+//
//
// B) Inspecting the output
//
// > ls klee-last/
//
// [your answer here]
+// assembly.ll info messages.txt run.istats run.stats
+// test000001.ktest test000002.ktest test000003.ktest warnings.txt
//
// C) Inspecting the generated test cases
//
@@ -45,17 +53,57 @@ int main()
// What path in the code does this test represent?
//
// [your answer here]
+// ktest file : 'klee-last/test000001.ktest'
+// args : ['get_sign.bc']
+// num objects: 1
+// object 0: name: 'a'
+// object 0: size: 4
+// object 0: data: b'\x00\x00\x00\x00'
+// object 0: hex : 0x00000000
+// object 0: int : 0
+// object 0: uint: 0
+// object 0: text: ....
+//
+// It represent the path where x = 0 and the return value is 0.
+//
//
// > ktest-tool klee-last/test000002.ktest
//
// What path in the code does this test represent?
//
// [your answer here]
+// ktest file : 'klee-last/test000002.ktest'
+// args : ['get_sign.bc']
+// num objects: 1
+// object 0: name: 'a'
+// object 0: size: 4
+// object 0: data: b'\x01\x01\x01\x01'
+// object 0: hex : 0x01010101
+// object 0: int : 16843009
+// object 0: uint: 16843009
+// object 0: text: ....
+//
+// It represent the path where x > 0 and the return value is 1.
+//
+//
// > ktest-tool klee-last/test000003.ktest
//
// What path in the code does this test represent?
//
// [your answer here]
+// ktest file : 'klee-last/test000003.ktest'
+// args : ['get_sign.bc']
+// num objects: 1
+// object 0: name: 'a'
+// object 0: size: 4
+// object 0: data: b'\x02\x01\x01\x80'
+// object 0: hex : 0x02010180
+// object 0: int : -2147417854
+// object 0: uint: 2147549442
+// object 0: text: ....
+//
+// It represent the path where x < 0 and the return value is -1.
+//
//
// D) Replaying a test case
//
@@ -109,6 +157,8 @@ int main()
// Did the result correspond to the expected path for the test?
//
// [your answer here]
+// yes
+// echo $? gives 0
//
// > KTEST_FILE=klee-last/test000002.ktest ./a.out
//
@@ -117,6 +167,8 @@ int main()
// Did the result correspond to the expected path for the test?
//
// [your answer here]
+// Yes
+// echo $? gives 1
//
// > KTEST_FILE=klee-last/test000003.ktest ./a.out
//
@@ -125,10 +177,13 @@ int main()
// Did the result correspond to the expected path for the test?
//
// [your answer here]
+// Yes
+// echo $? gives 255 (which is equal to -1 of 8 signed bits)
//
// Why not? Confer to shell error codes:
//
// [your answer here]
+// ??? TODO
//
// D) Debugging
//
@@ -153,6 +208,9 @@ int main()
// What value do you get, and why?
//
// [your answer here]
+// (gdb) print x
+// $1 = 0
+// It has the value 0 and it got that because the constraint x == o is the fist split in the paths.
//
// Step the code
// > (gdb) next
@@ -160,6 +218,12 @@ int main()
// What path did it take, and why?
//
// [your answer here]
+// Breakpoint 1, get_sign (x=0) at get_sign.c:10
+// 10 if (x == 0)
+// (gdb) next
+// 11 return 0;
+// It took the path where it returns 0.
+// It took that path because x = 0 thus x == 0.
//
// Now we can try with another test:
//
@@ -173,6 +237,15 @@ int main()
// Which path did it take, and why?
//
// [your answer here]
+// Breakpoint 1, get_sign (x=16843009) at get_sign.c:10
+// 10 if (x == 0)
+// (gdb) next
+// 13 if (x < 0)
+// (gdb) next
+// 16 return 1;
+// It took the path where it returns 1.
+// It took that path because x = 16843009 thus x != 0 and x !< 0.
+//
//
// And finally:
//
@@ -181,6 +254,14 @@ int main()
// Which path did it take, and why?
//
// [your answer here]
+// Breakpoint 1, get_sign (x=-2147417854) at get_sign.c:10
+// 10 if (x == 0)
+// (gdb) next
+// 13 if (x < 0)
+// (gdb) next
+// 14 return -1;
+// It took the path where it returns -1.
+// It took that path because x = -2147417854 thus x != 0 and x < 0.
//
// E) Under the hood.
//
diff --git a/examples/klee-last b/examples/klee-last
new file mode 120000
index 0000000000000000000000000000000000000000..c01e6451b12d8641916ad2be4999212cfbc63164
--- /dev/null
+++ b/examples/klee-last
@@ -0,0 +1 @@
+/home/niklas/Desktop/D7020E/klee_tutorial/examples/klee-out-0
\ No newline at end of file
diff --git a/examples/klee-out-0/assembly.ll b/examples/klee-out-0/assembly.ll
new file mode 100644
index 0000000000000000000000000000000000000000..539e6b61e53f21e6c50c6d4e0c17680b6cafef92
--- /dev/null
+++ b/examples/klee-out-0/assembly.ll
@@ -0,0 +1,60 @@
+; ModuleID = 'get_sign.bc'
+source_filename = "get_sign.c"
+target datalayout = "e-m:e-i64:64-f80:128-n8:16:32:64-S128"
+target triple = "x86_64-pc-linux-gnu"
+
+@.str = private unnamed_addr constant [2 x i8] c"a\00", align 1
+
+; Function Attrs: noinline nounwind optnone uwtable
+define dso_local i32 @get_sign(i32) #0 {
+ %2 = alloca i32, align 4
+ %3 = alloca i32, align 4
+ store i32 %0, i32* %3, align 4
+ %4 = load i32, i32* %3, align 4
+ %5 = icmp eq i32 %4, 0
+ br i1 %5, label %6, label %7
+
+6: ; preds = %1
+ store i32 0, i32* %2, align 4
+ br label %12
+
+7: ; preds = %1
+ %8 = load i32, i32* %3, align 4
+ %9 = icmp slt i32 %8, 0
+ br i1 %9, label %10, label %11
+
+10: ; preds = %7
+ store i32 -1, i32* %2, align 4
+ br label %12
+
+11: ; preds = %7
+ store i32 1, i32* %2, align 4
+ br label %12
+
+12: ; preds = %11, %10, %6
+ %13 = load i32, i32* %2, align 4
+ ret i32 %13
+}
+
+; Function Attrs: noinline nounwind optnone uwtable
+define dso_local i32 @main() #0 {
+ %1 = alloca i32, align 4
+ %2 = alloca i32, align 4
+ store i32 0, i32* %1, align 4
+ %3 = bitcast i32* %2 to i8*
+ call void @klee_make_symbolic(i8* %3, i64 4, i8* getelementptr inbounds ([2 x i8], [2 x i8]* @.str, i64 0, i64 0))
+ %4 = load i32, i32* %2, align 4
+ %5 = call i32 @get_sign(i32 %4)
+ ret i32 %5
+}
+
+declare dso_local void @klee_make_symbolic(i8*, i64, i8*) #1
+
+attributes #0 = { noinline nounwind optnone uwtable "correctly-rounded-divide-sqrt-fp-math"="false" "disable-tail-calls"="false" "less-precise-fpmad"="false" "min-legal-vector-width"="0" "no-frame-pointer-elim"="true" "no-frame-pointer-elim-non-leaf" "no-infs-fp-math"="false" "no-jump-tables"="false" "no-nans-fp-math"="false" "no-signed-zeros-fp-math"="false" "no-trapping-math"="false" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+cx8,+fxsr,+mmx,+sse,+sse2,+x87" "unsafe-fp-math"="false" "use-soft-float"="false" }
+attributes #1 = { "correctly-rounded-divide-sqrt-fp-math"="false" "disable-tail-calls"="false" "less-precise-fpmad"="false" "no-frame-pointer-elim"="true" "no-frame-pointer-elim-non-leaf" "no-infs-fp-math"="false" "no-nans-fp-math"="false" "no-signed-zeros-fp-math"="false" "no-trapping-math"="false" "stack-protector-buffer-size"="8" "target-cpu"="x86-64" "target-features"="+cx8,+fxsr,+mmx,+sse,+sse2,+x87" "unsafe-fp-math"="false" "use-soft-float"="false" }
+
+!llvm.module.flags = !{!0}
+!llvm.ident = !{!1}
+
+!0 = !{i32 1, !"wchar_size", i32 4}
+!1 = !{!"clang version 9.0.0-2 (tags/RELEASE_900/final)"}
diff --git a/examples/klee-out-0/info b/examples/klee-out-0/info
new file mode 100644
index 0000000000000000000000000000000000000000..09ca2de8351f06c010729994441aff081f3b52c6
--- /dev/null
+++ b/examples/klee-out-0/info
@@ -0,0 +1,22 @@
+klee get_sign.bc
+PID: 31615
+Using monotonic steady clock with 1/1000000000s resolution
+Started: 2020-12-07 17:08:04
+BEGIN searcher description
+<InterleavedSearcher> containing 2 searchers:
+RandomPathSearcher
+WeightedRandomSearcher::CoveringNew
+</InterleavedSearcher>
+END searcher description
+Finished: 2020-12-07 17:08:04
+Elapsed: 00:00:00
+KLEE: done: explored paths = 3
+KLEE: done: avg. constructs per query = 11
+KLEE: done: total queries = 3
+KLEE: done: valid queries = 0
+KLEE: done: invalid queries = 3
+KLEE: done: query cex = 3
+
+KLEE: done: total instructions = 31
+KLEE: done: completed paths = 3
+KLEE: done: generated tests = 3
diff --git a/examples/klee-out-0/messages.txt b/examples/klee-out-0/messages.txt
new file mode 100644
index 0000000000000000000000000000000000000000..d49ad73298ce077c15ada9b7d55fa15a59692adf
--- /dev/null
+++ b/examples/klee-out-0/messages.txt
@@ -0,0 +1 @@
+KLEE: Using Z3 solver backend
diff --git a/examples/klee-out-0/run.istats b/examples/klee-out-0/run.istats
new file mode 100644
index 0000000000000000000000000000000000000000..f5382c7ebbba74eb0a096bed3ef917393ba8b382
--- /dev/null
+++ b/examples/klee-out-0/run.istats
@@ -0,0 +1,52 @@
+version: 1
+creator: klee
+pid: 31615
+cmd: get_sign.bc
+
+
+positions: instr line
+event: Icov : CoveredInstructions
+event: Forks : Forks
+event: Ireal : InstructionRealTimes
+event: Itime : InstructionTimes
+event: I : Instructions
+event: UCdist : MinDistToUncovered
+event: Rtime : ResolveTime
+event: States : States
+event: Iuncov : UncoveredInstructions
+event: Q : Queries
+event: Qiv : QueriesInvalid
+event: Qv : QueriesValid
+event: Qtime : QueryTime
+events: Icov Forks Ireal Itime I UCdist Rtime States Iuncov Q Qiv Qv Qtime
+ob=assembly.ll
+fn=get_sign
+10 0 1 0 0 0 1 0 0 0 0 0 0 0 0
+11 0 1 0 0 0 1 0 0 0 0 0 0 0 0
+12 0 1 0 0 0 1 0 0 0 0 0 0 0 0
+13 0 1 0 0 0 1 0 0 0 0 0 0 0 0
+14 0 1 0 0 0 1 0 0 0 0 0 0 0 0
+15 0 1 1 0 0 1 0 0 0 0 2 2 0 40035
+18 0 1 0 0 0 1 0 0 0 0 0 0 0 0
+19 0 1 0 0 0 1 0 0 0 0 0 0 0 0
+22 0 1 0 0 0 1 0 0 0 0 0 0 0 0
+23 0 1 0 0 0 1 0 0 0 0 0 0 0 0
+24 0 1 1 0 0 1 0 0 0 0 1 1 0 18179
+27 0 1 0 0 0 1 0 0 0 0 0 0 0 0
+28 0 1 0 0 0 1 0 0 0 0 0 0 0 0
+31 0 1 0 0 0 1 0 0 0 0 0 0 0 0
+32 0 1 0 0 0 1 0 0 0 0 0 0 0 0
+35 0 1 0 0 0 3 0 0 0 0 0 0 0 0
+36 0 1 0 0 0 3 0 0 0 0 0 0 0 0
+fn=main
+41 0 1 0 0 0 1 0 0 0 0 0 0 0 0
+42 0 1 0 0 0 1 0 0 0 0 0 0 0 0
+43 0 1 0 0 0 1 0 0 0 0 0 0 0 0
+44 0 1 0 0 0 1 0 0 0 0 0 0 0 0
+45 0 1 0 0 0 1 0 0 0 0 0 0 0 0
+46 0 1 0 0 0 1 0 0 0 0 0 0 0 0
+47 0 1 0 0 0 1 0 0 0 0 0 0 0 0
+cfn=get_sign
+calls=1 8 0
+47 0 17 2 0 0 21 0 0 0 0 3 3 0 58214
+48 0 1 0 0 0 3 0 0 0 0 0 0 0 0
diff --git a/examples/klee-out-0/run.stats b/examples/klee-out-0/run.stats
new file mode 100644
index 0000000000000000000000000000000000000000..b413870ae189c7361e1d9086008db3a48468e89f
Binary files /dev/null and b/examples/klee-out-0/run.stats differ
diff --git a/examples/klee-out-0/test000001.ktest b/examples/klee-out-0/test000001.ktest
new file mode 100644
index 0000000000000000000000000000000000000000..25f74a85d90a98ba12009cab156dd058ea9079b6
Binary files /dev/null and b/examples/klee-out-0/test000001.ktest differ
diff --git a/examples/klee-out-0/test000002.ktest b/examples/klee-out-0/test000002.ktest
new file mode 100644
index 0000000000000000000000000000000000000000..48f5296d51ace0720bc14608c18a4035225a2b3e
Binary files /dev/null and b/examples/klee-out-0/test000002.ktest differ
diff --git a/examples/klee-out-0/test000003.ktest b/examples/klee-out-0/test000003.ktest
new file mode 100644
index 0000000000000000000000000000000000000000..d3902760c5771dec64d1bf50b3cbf5b8c13aa77d
Binary files /dev/null and b/examples/klee-out-0/test000003.ktest differ
diff --git a/examples/klee-out-0/warnings.txt b/examples/klee-out-0/warnings.txt
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391