diff --git a/src/nagini_translation/main.py b/src/nagini_translation/main.py
index e816c80a5..2363456a2 100644
--- a/src/nagini_translation/main.py
+++ b/src/nagini_translation/main.py
@@ -97,7 +97,10 @@ def translate(path: str, jvm: JVM, selected: Set[str] = set(), base_dir: str = N
     path = os.path.abspath(path)
     error_manager.clear()
     current_path = os.path.dirname(inspect.stack()[0][1])
-    resources_path = os.path.join(current_path, 'resources')
+    if sif:
+        preamble_path = os.path.join(current_path, 'sif', 'resources')
+    else:
+        preamble_path = os.path.join(current_path, 'resources')
 
     if sif:
         viper_ast = ViperASTExtended(jvm, jvm.java, jvm.scala, jvm.viper, path)
@@ -114,7 +117,7 @@ def translate(path: str, jvm: JVM, selected: Set[str] = set(), base_dir: str = N
 
     analyzer = Analyzer(types, path, selected)
     main_module = analyzer.module
-    with open(os.path.join(resources_path, 'preamble.index'), 'r') as file:
+    with open(os.path.join(preamble_path, 'preamble.index'), 'r') as file:
         analyzer.add_native_silver_builtins(json.loads(file.read()))
 
     analyzer.initialize_io_analyzer()
diff --git a/src/nagini_translation/resources/all.sil b/src/nagini_translation/resources/all.sil
index 33ea0ca7e..a61f76d7f 100644
--- a/src/nagini_translation/resources/all.sil
+++ b/src/nagini_translation/resources/all.sil
@@ -12,10 +12,15 @@ domain SIFDomain[T] {
     axiom low_true {
         forall x: T :: {Low(x)} Low(x)
     }
+    axiom lowevent_true {
+        LowEvent()
+    }
+    function LowEvent(): Bool
 }
 
 
 import "bool.sil"
+import "references.sil"
 import "bytes.sil"
 import "iterator.sil"
 import "list.sil"
diff --git a/src/nagini_translation/resources/backends/silver-sif-extension.jar b/src/nagini_translation/resources/backends/silver-sif-extension.jar
index 686b75e30..4e38f9859 100644
Binary files a/src/nagini_translation/resources/backends/silver-sif-extension.jar and b/src/nagini_translation/resources/backends/silver-sif-extension.jar differ
diff --git a/src/nagini_translation/resources/bool.sil b/src/nagini_translation/resources/bool.sil
index bc0daa373..2aefc63b8 100644
--- a/src/nagini_translation/resources/bool.sil
+++ b/src/nagini_translation/resources/bool.sil
@@ -18,10 +18,6 @@ function NoneType___bool__(self: Ref) : Bool
     decreases _
     ensures self == null ==> !result
 
-function object___str__(self: Ref) : Ref
-    decreases _
-    ensures issubtype(typeof(result), str())
-
 function bool___bool__(self: Ref) : Bool
     decreases _
     requires self != null ==> issubtype(typeof(self), bool())
@@ -258,4 +254,6 @@ function abs(a: Int): Int
     decreases _
     ensures result == (a >= 0 ? a : -a)
 
-method print(r: Ref)
\ No newline at end of file
+method print(r: Ref)
+    requires Low(r)
+    requires LowEvent()
\ No newline at end of file
diff --git a/src/nagini_translation/resources/references.sil b/src/nagini_translation/resources/references.sil
new file mode 100644
index 000000000..bd944557b
--- /dev/null
+++ b/src/nagini_translation/resources/references.sil
@@ -0,0 +1,11 @@
+/*
+ * Copyright (c) 2019 ETH Zurich
+ * This Source Code Form is subject to the terms of the Mozilla Public
+ * License, v. 2.0. If a copy of the MPL was not distributed with this
+ * file, You can obtain one at http://mozilla.org/MPL/2.0/.
+ */
+
+
+ function object___str__(self: Ref) : Ref
+    decreases _
+    ensures issubtype(typeof(result), str())
\ No newline at end of file
diff --git a/src/nagini_translation/sif/resources/all.sil b/src/nagini_translation/sif/resources/all.sil
index d5e032e6a..58d47c9de 100644
--- a/src/nagini_translation/sif/resources/all.sil
+++ b/src/nagini_translation/sif/resources/all.sil
@@ -5,11 +5,15 @@
  * file, You can obtain one at http://mozilla.org/MPL/2.0/.
  */
 
+import <decreases/int.vpr>
+
 domain SIFDomain[T] {
     function Low(x: T): Bool
+    function LowEvent(): Bool
 }
 
 import "../../resources/bool.sil"
+import "references.sil"
 import "../../resources/bytes.sil"
 import "../../resources/iterator.sil"
 import "../../resources/list.sil"
diff --git a/src/nagini_translation/sif/resources/preamble.index b/src/nagini_translation/sif/resources/preamble.index
new file mode 100644
index 000000000..4f8551d20
--- /dev/null
+++ b/src/nagini_translation/sif/resources/preamble.index
@@ -0,0 +1,897 @@
+{
+"object": {
+    "functions": {
+        "__bool__": {
+            "args": ["object"],
+            "type": "__prim__bool",
+            "requires": ["list", "list_arg", "set", "set_arg", "dict", "dict_arg"]
+        },
+        "__eq__": {
+            "args": ["object", "object"],
+            "type": "__prim__bool"
+        },
+        "__cast__": {
+            "args": ["type", "object"],
+            "type": "object"
+        }
+    },
+    "methods": {
+        "__str__": {
+            "args": ["object"],
+            "type": "str",
+            "MustTerminate": true
+        }
+    }
+},
+"list": {
+    "methods": {
+        "__init__": {
+            "args": [],
+            "type": null,
+            "MustTerminate": true
+        },
+        "append": {
+            "args": ["list", "object"],
+            "type": null,
+            "requires": ["__sil_seq__"],
+            "MustTerminate": true
+        },
+        "extend": {
+            "args": ["list", "list"],
+            "type": null,
+            "MustTerminate": true
+        },
+        "reverse": {
+            "args": ["list"],
+            "type": "list",
+            "MustTerminate": true
+        },
+        "__setitem__": {
+            "args": ["list", "__prim__int", "object"],
+            "type": null,
+            "MustTerminate": true,
+            "requires": ["__len__"]
+        },
+        "__iter__": {
+            "args": ["list"],
+            "type": "Iterator",
+            "MustTerminate": true
+        },
+        "__getitem_slice__": {
+            "args": ["list", "slice"],
+            "type": "list",
+            "display_name": "__getitem__",
+            "requires": ["__len__", "slice___start__", "slice___stop__"],
+            "MustTerminate": true
+        },
+        "__add__": {
+            "args": ["list", "list"],
+            "type": "list",
+            "MustTerminate": true
+        },
+        "__mul__": {
+            "args": ["list", "__prim__int"],
+            "type": "list",
+            "MustTerminate": true
+        }
+    },
+    "functions": {
+        "__getitem__": {
+            "args": ["list", "int"],
+            "type": "object",
+            "requires": ["__len__"]
+        },
+        "__contains__": {
+            "args": ["list", "object"],
+            "type": "__prim__bool"
+        },
+        "__len__": {
+            "args": ["list"],
+            "type": "__prim__int"
+        },
+        "__bool__": {
+            "args": ["list"],
+            "type": "__prim__bool"
+        },
+        "__sil_seq__": {
+            "args": ["list"],
+            "type": "__prim__Seq"
+        }
+    },
+    "type_vars": 1,
+    "extends": "object",
+    "generate_sif": true
+},
+"set":{
+    "methods": {
+        "__init__": {
+            "args": [],
+            "type": null,
+            "MustTerminate": true
+        },
+        "add": {
+            "args": ["set", "object"],
+            "type": null,
+            "MustTerminate": true
+        },
+        "remove": {
+            "args": ["set", "object"],
+            "type": null,
+            "MustTerminate": true
+        },
+        "clear": {
+            "args": ["set"],
+            "type": null,
+            "MustTerminate": true
+        },
+        "__iter__": {
+            "args": ["set"],
+            "type": "Iterator",
+            "MustTerminate": true,
+            "requires": ["__sil_seq__"]
+        }
+    },
+    "functions": {
+        "__contains__": {
+            "args": ["dict", "object"],
+            "type": "__prim__bool"
+        },
+        "__bool__": {
+            "args": ["set"],
+            "type": "__prim__bool"
+        },
+        "__len__": {
+            "args": ["set"],
+            "type": "__prim__int"
+        },
+        "__sil_seq__": {
+            "args": ["set"],
+            "type": "__prim__Seq"
+        }
+    },
+    "type_vars": 1,
+    "extends": "object"
+},
+"dict": {
+    "methods": {
+        "__init__": {
+            "args": [],
+            "type": null,
+            "MustTerminate": true
+        },
+        "keys": {
+            "args": ["dict"],
+            "type": "set",
+            "MustTerminate": true
+        },
+        "__setitem__": {
+            "args": ["dict", "object", "object"],
+            "type": null,
+            "MustTerminate": true,
+            "requires": ["__getitem__", "__contains__"]
+        },
+        "__iter__": {
+            "args": ["dict"],
+            "type": "Iterator",
+            "MustTerminate": true,
+            "requires": ["__sil_seq__"]
+        },
+        "values": {
+            "args": ["dict"],
+            "type": "list",
+            "MustTerminate": true,
+            "requires": ["__contains__", "__getitem__"]
+        }
+    },
+    "functions": {
+        "__contains__": {
+            "args": ["dict", "object"],
+            "type": "__prim__bool"
+        },
+        "__getitem__": {
+            "args": ["dict", "object"],
+            "type": "object",
+            "requires": ["__contains__"]
+        },
+        "get": {
+            "args": ["dict", "object"],
+            "type": "object",
+            "generic_type": 1,
+            "requires": ["__contains__", "__getitem__"]
+        },
+        "__bool__": {
+            "args": ["dict"],
+            "type": "__prim__bool"
+        },
+        "__len__": {
+            "args": ["dict"],
+            "type": "__prim__int"
+        },
+        "__sil_seq__": {
+            "args": ["dict"],
+            "type": "__prim__Seq"
+        }
+    },
+    "type_vars": 2,
+    "extends": "object"
+},
+"int": {
+    "functions": {
+        "__bool__": {
+            "args": ["int"],
+            "type": "__prim__bool"
+        },
+        "__unbox__": {
+            "args": ["int"],
+            "type": "__prim__int",
+            "requires": ["__prim__int___box__", "__prim__bool___box__"]
+        },
+        "__eq__": {
+            "args": ["int", "object"],
+            "type": "__prim__bool",
+            "requires": ["__unbox__"]
+        },
+        "__add__": {
+            "args": ["__prim__int", "__prim__int"],
+            "type": "__prim__int"
+        },
+        "__sub__": {
+            "args": ["__prim__int", "__prim__int"],
+            "type": "__prim__int",
+            "requires": ["__unbox__"]
+        },
+        "__mul__": {
+            "args": ["__prim__int", "__prim__int"],
+            "type": "__prim__int"
+        },
+        "__div__": {
+            "args": ["__prim__int", "__prim__int"],
+            "type": "float"
+        },
+        "__floordiv__": {
+            "args": ["__prim__int", "__prim__int"],
+            "type": "__prim__int"
+        },
+        "__mod__": {
+            "args": ["__prim__int", "__prim__int"],
+            "type": "__prim__int"
+        },
+        "__ge__": {
+            "args": ["__prim__int", "__prim__int"],
+            "type": "__prim__bool"
+        },
+        "__gt__": {
+            "args": ["__prim__int", "__prim__int"],
+            "type": "__prim__bool"
+        },
+        "__lt__": {
+            "args": ["__prim__int", "__prim__int"],
+            "type": "__prim__bool"
+        },
+        "__le__": {
+            "args": ["__prim__int", "__prim__int"],
+            "type": "__prim__bool"
+        },
+        "__int__": {
+            "args": ["int"],
+            "type": "int"
+        }
+    },
+    "extends": "float"
+},
+"float": {
+    "functions": {
+        "__create__": {
+            "args": ["__prim__int"],
+            "type": "float"
+        },
+        "__bool__": {
+            "args": ["float"],
+            "type": "__prim__bool",
+            "requires": ["int___bool__", "int___unbox__"]
+        },
+        "__eq__": {
+            "args": ["float", "object"],
+            "type": "__prim__bool",
+            "requires": ["int___eq__"]
+        },
+        "__add__": {
+            "args": ["float", "float"],
+            "type": "float",
+            "requires": ["int___add__", "int___unbox__"]
+        },
+        "__sub__": {
+            "args": ["float", "float"],
+            "type": "float",
+            "requires": ["int___sub__", "int___unbox__"]
+        },
+        "__mul__": {
+            "args": ["float", "float"],
+            "type": "float",
+            "requires": ["int___mul__", "int___unbox__"]
+        },
+        "__div__": {
+            "args": ["float", "float"],
+            "type": "float",
+            "requires": ["int___div__", "int___unbox__"]
+        },
+        "__ge__": {
+            "args": ["float", "float"],
+            "type": "__prim__bool",
+            "requires": ["int___ge__", "int___unbox__"]
+        },
+        "__gt__": {
+            "args": ["float", "float"],
+            "type": "__prim__bool",
+            "requires": ["int___gt__", "int___unbox__"]
+        },
+        "__lt__": {
+            "args": ["float", "float"],
+            "type": "__prim__bool",
+            "requires": ["int___lt__", "int___unbox__"]
+        },
+        "__le__": {
+            "args": ["float", "float"],
+            "type": "__prim__bool",
+            "requires": ["int___le__", "int___unbox__"]
+        },
+        "__int__": {
+            "args": ["float"],
+            "type": "int"
+        }
+    },
+    "extends": "object"
+},
+"bool": {
+    "functions": {
+        "__unbox__": {
+            "args": ["bool"],
+            "type": "__prim__bool",
+            "requires": ["__prim__bool___box__"]
+        },
+        "__bool__": {
+            "args": ["bool"],
+            "type": "__prim__bool"
+        },
+        "__eq__": {
+            "args": ["bool", "object"],
+            "type": "__prim__bool",
+            "requires": ["__unbox__"]
+        }
+    },
+    "extends": "int"
+},
+"NoneType": {
+    "functions": {
+        "__bool__": {
+            "args": ["object"],
+            "type": "__prim__bool"
+        }
+    },
+    "extends": "object"
+},
+"Exception": {
+    "extends": "object"
+},
+"ConnectionRefusedError": {
+    "extends": "Exception"
+},
+"traceback": {
+    "extends": "object"
+},
+"str": {
+    "functions": {
+        "__len__": {
+            "args": ["str"],
+            "type": "__prim__int"
+        },
+        "__bool__": {
+            "args": ["str"],
+            "type": "__prim__bool",
+            "requires": ["__len__"]
+        },
+        "__eq__": {
+            "args": ["str", "object"],
+            "type": "__prim__bool"
+        },
+        "__add__": {
+            "args": ["str", "str"],
+            "type": "str"
+        },
+        "__create__": {
+            "args": ["__prim__int", "__prim__int"],
+            "type": "str",
+            "requires": ["__len__", "__val__"]
+        },
+        "__val__": {
+            "args": ["str"],
+            "type": "int"
+        },
+        "join": {
+            "args": ["str", "list"],
+            "type": "str"
+        },
+        "__mod__": {
+            "args": ["str", "tuple"],
+            "type": "str"
+        }
+    },
+    "methods": {
+        "split": {
+            "args": ["str"],
+            "type": "list",
+            "MustTerminate": true
+        }
+    },
+    "extends": "object"
+},
+"bytes": {
+    "functions": {
+        "__len__": {
+            "args": ["bytes"],
+            "type": "__prim__int",
+            "requires": ["__val__"]
+        },
+        "__bool__": {
+            "args": ["bytes"],
+            "type": "__prim__bool",
+            "requires": ["__len__"]
+        },
+        "__eq__": {
+            "args": ["bytes", "object"],
+            "type": "__prim__bool",
+            "requires": ["__val__", "__len__"]
+        },
+        "__add__": {
+            "args": ["bytes", "bytes"],
+            "type": "bytes",
+            "requires": ["__val__", "__len__"]
+        },
+        "__mul__": {
+            "args": ["bytes", "__prim__int"],
+            "type": "bytes",
+            "requires": ["__val__", "__len__", "bytes___mul__helper"]
+        },
+        "__sil_seq__": {
+            "args": ["bytes"],
+            "type": "__prim__Seq",
+            "requires": ["__val__"]
+        },
+        "__create__": {
+            "args": ["__prim__Seq", "__prim__int"],
+            "type": "bytes",
+            "requires": ["__len__", "__val__"]
+        },
+        "__val__": {
+            "args": ["bytes"],
+            "type": "__prim__Seq"
+        },
+        "__getitem_slice__": {
+            "args": ["bytes", "slice"],
+            "type": "int",
+            "display_name": "__getitem__",
+            "requires": ["__len__", "__val__", "slice___start__", "slice___stop__"]
+        },
+        "__getitem__": {
+            "args": ["bytes", "__prim__int"],
+            "type": "int",
+            "requires": ["__len__", "__val__"]
+        },
+        "join": {
+            "args": ["bytes", "list"],
+            "type": "bytes",
+            "requires": ["__val__", "__len__", "bytes_join_val_helper", "list___len__", "list___getitem__"]
+        }
+    },
+    "extends": "object"
+},
+"tuple": {
+    "functions": {
+        "__create0__": {
+            "args": [],
+            "type": "tuple",
+            "requires": ["__val__", "__len__"]
+        },
+        "__create__": {
+            "args": ["__prim__Seq", "__prim__Seq_type", "__prim__int"],
+            "type": "tuple",
+            "requires": ["__val__", "__len__"]
+        },
+        "__create1__": {
+            "args": ["object", "type", "__prim__int"],
+            "type": "tuple",
+            "requires": ["__len__", "__getitem__"]
+        },
+        "__create2__": {
+            "args": ["object", "object", "type", "type", "__prim__int"],
+            "type": "tuple",
+            "requires": ["__len__", "__getitem__"]
+        },
+        "__create3__": {
+            "args": ["object", "object", "object", "type", "type", "type", "__prim__int"],
+            "type": "tuple",
+            "requires": ["__len__", "__getitem__"]
+        },
+        "__create4__": {
+            "args": ["object", "object", "object", "object", "type", "type", "type", "type", "__prim__int"],
+            "type": "tuple",
+            "requires": ["__len__", "__getitem__"]
+        },
+        "__create5__": {
+            "args": ["object", "object", "object", "object", "object", "type", "type", "type", "type", "type", "__prim__int"],
+            "type": "tuple",
+            "requires": ["__len__", "__getitem__"]
+        },
+        "__create6__": {
+            "args": ["object", "object", "object", "object", "object", "object", "type", "type", "type", "type", "type", "type", "__prim__int"],
+            "type": "tuple",
+            "requires": ["__len__", "__getitem__"]
+        },
+        "__getitem__": {
+            "args": ["tuple", "__prim__int"],
+            "type": "object",
+            "requires": ["__len__", "__val__", "__len__"]
+        },
+        "__getitem_slice__": {
+            "args": ["tuple", "slice"],
+            "type": "object",
+            "display_name": "__getitem__",
+            "requires": ["__len__", "__getitem__", "__val__", "slice___start__", "slice___stop__"]
+        },
+        "__contains__": {
+            "args": ["tuple", "object"],
+            "type": "__prim__bool",
+            "requires": ["__val__"]
+        },
+        "__len__": {
+            "args": ["tuple"],
+            "type": "__prim__int",
+            "requires": ["__val__", "args"]
+        },
+        "__val__": {
+            "args": ["tuple"],
+            "type": "__prim__Seq"
+        },
+        "__eq__": {
+            "args": ["tuple", "object"],
+            "type": "__prim__bool",
+            "requires": ["__len__", "__getitem__"]
+        },
+        "__sil_seq__": {
+            "args": ["tuple"],
+            "type": "__prim__Seq",
+            "requires": ["__len__", "__val__"]
+        }
+    },
+    "type_vars": -1,
+    "extends": "object"
+},
+"__prim__int": {
+    "functions": {
+        "__box__": {
+            "args": ["__prim__int"],
+            "type": "int",
+            "requires": ["int___unbox__"]
+        }
+    }
+},
+"__prim__bool": {
+    "functions": {
+        "__box__": {
+            "args": ["__prim__bool"],
+            "type": "bool",
+            "requires": ["bool___unbox__", "int___unbox__"]
+        }
+    }
+},
+"__prim__Seq": {},
+"__prim__Set": {},
+"__prim__Multiset": {},
+"PSeq": {
+    "functions": {
+        "__create__": {
+            "args": ["__prim__Seq", "type"],
+            "type": "PSeq",
+            "requires": ["__sil_seq__"]
+        },
+        "__unbox__": {
+            "args": ["PSeq"],
+            "type": "__prim__Seq",
+            "requires": []
+        },
+        "__contains__": {
+            "args": ["PSeq", "object"],
+            "type": "__prim__bool",
+            "requires": ["__sil_seq__"]
+        },
+        "__getitem__": {
+            "args": ["PSeq", "int"],
+            "type": "object",
+            "requires": ["__sil_seq__", "__len__", "int___unbox__"]
+        },
+        "__sil_seq__": {
+            "args": ["PSeq"],
+            "type": "__prim__Seq"
+        },
+        "__len__": {
+            "args": ["PSeq"],
+            "type": "__prim__int",
+            "requires": ["__sil_seq__"]
+        },
+        "take": {
+            "args": ["PSeq", "__prim__int"],
+            "type": "PSeq",
+            "generic_type": -2,
+            "requires": ["__sil_seq__", "__create__"]
+        },
+        "drop": {
+            "args": ["PSeq", "__prim__int"],
+            "type": "PSeq",
+            "generic_type": -2,
+            "requires": ["__sil_seq__", "__create__"]
+        },
+        "update": {
+            "args": ["PSeq", "__prim__int", "object"],
+            "type": "PSeq",
+            "requires": ["__sil_seq__", "__create__"]
+        },
+        "__add__": {
+            "args": ["PSeq", "PSeq"],
+            "type": "PSeq",
+            "requires": ["__sil_seq__", "__create__"]
+        },
+        "__eq__": {
+            "args": ["PSeq", "PSeq"],
+            "type": "__prim__bool",
+            "requires": ["__sil_seq__"]
+        }
+    },
+    "type_vars": 1,
+    "extends": "object"
+},
+"PSet": {
+    "functions": {
+        "__create__": {
+            "args": ["__prim__Set", "type"],
+            "type": "PSet",
+            "requires": ["__unbox__"]
+        },
+        "__unbox__": {
+            "args": ["PSet"],
+            "type": "__prim__Set",
+            "requires": []
+        },
+        "__contains__": {
+            "args": ["PSet", "object"],
+            "type": "__prim__bool",
+            "requires": ["__unbox__"]
+        },
+        "__sil_seq__": {
+            "args": ["PSet"],
+            "type": "__prim__Seq",
+            "requires": ["__unbox__"]
+        },
+        "__len__": {
+            "args": ["PSet"],
+            "type": "__prim__int",
+            "requires": ["__unbox__"]
+        },
+        "__add__": {
+            "args": ["PSet", "PSet"],
+            "type": "PSet",
+            "requires": ["__unbox__", "__create__"]
+        },
+        "__sub__": {
+            "args": ["PSet", "PSet"],
+            "type": "PSet",
+            "requires": ["__unbox__", "__create__"]
+        },
+        "__eq__": {
+            "args": ["PSet", "PSet"],
+            "type": "__prim__bool",
+            "requires": ["__unbox__"]
+        }
+    },
+    "type_vars": 1,
+    "extends": "object"
+},
+"PMultiset": {
+    "functions": {
+        "__create__": {
+            "args": ["__prim__Multiset", "type"],
+            "type": "PMultiset",
+            "requires": ["__unbox__"]
+        },
+        "__unbox__": {
+            "args": ["PMultiset"],
+            "type": "__prim__Multiset",
+            "requires": []
+        },
+        "num": {
+            "args": ["PMultiset", "object"],
+            "type": "__prim__int",
+            "requires": ["__unbox__"]
+        },
+        "__sil_seq__": {
+            "args": ["PMultiset"],
+            "type": "__prim__Seq",
+            "requires": ["__unbox__"]
+        },
+        "__len__": {
+            "args": ["PMultiset"],
+            "type": "__prim__int",
+            "requires": ["__unbox__"]
+        },
+        "__add__": {
+            "args": ["PMultiset", "PMultiset"],
+            "type": "PMultiset",
+            "requires": ["__unbox__", "__create__"]
+        },
+        "__sub__": {
+            "args": ["PMultiset", "PMultiset"],
+            "type": "PMultiset",
+            "requires": ["__unbox__", "__create__"]
+        },
+        "__eq__": {
+            "args": ["PMultiset", "PMultiset"],
+            "type": "__prim__bool",
+            "requires": ["__unbox__"]
+        }
+    },
+    "type_vars": 1,
+    "extends": "object"
+},
+"slice": {
+    "functions": {
+        "__create__": {
+            "args": ["int", "int"],
+            "type": "slice",
+            "requires": ["__internal_start__", "__internal_stop__"]
+        },
+        "__internal_start__": {
+            "args": ["slice"],
+            "type": "int"
+        },
+        "__internal_stop__": {
+            "args": ["slice"],
+            "type": "int"
+        },
+        "__start__": {
+            "args": ["slice"],
+            "type": "int",
+            "requires": ["__internal_start__"]
+        },
+        "__stop__": {
+            "args": ["slice"],
+            "type": "int",
+            "requires": ["__internal_stop__"]
+        }
+    },
+    "extends": "object"
+},
+"range": {
+    "functions": {
+        "__create__": {
+            "args": ["__prim__int", "__prim__int", "__prim__int"],
+            "type": "range",
+            "requires": ["__val__", "__start__", "__stop__"]
+        },
+        "__val__": {
+            "args": ["range"],
+            "type": "object"
+        },
+        "__start__": {
+            "args": ["range"],
+            "type": "object"
+        },
+        "__stop__": {
+            "args": ["range"],
+            "type": "object"
+        },
+        "__getitem__": {
+            "args": ["range", "__prim__int"],
+            "type": "__prim__int",
+            "requires": ["__val__"]
+        },
+        "__getitem_slice__": {
+            "args": ["range", "slice"],
+            "type": "range",
+            "display_name": "__getitem__",
+            "requires": ["__val__", "int___unbox__", "slice___start__", "slice___stop__"]
+        },
+        "__contains__": {
+            "args": ["range", "int"],
+            "type": "__prim__bool",
+            "requires": ["__sil_seq__"]
+        },
+        "__len__": {
+            "args": ["range"],
+            "type": "__prim__int",
+            "requires": ["__val__"]
+        },
+        "__bool__": {
+            "args": ["range"],
+            "type": "__prim__bool"
+        },
+        "__sil_seq__": {
+            "args": ["range"],
+            "type": "__prim__Seq",
+            "requires": ["__val__", "__len__", "__prim__int___box__", "int___unbox__", "__start__", "__stop__"]
+        },
+        "__eq__": {
+            "args": ["range", "object"],
+            "type": "__prim__bool",
+            "requires": ["__val__", "__len__"]
+        }
+    },
+    "methods": {
+        "__iter__": {
+            "args": ["range"],
+            "type": "Iterator",
+            "MustTerminate": true
+        }
+    },
+    "extends": "object"
+},
+"Iterator": {
+    "methods":{
+        "__next__": {
+            "args": ["Iterator"],
+            "type": "object",
+            "MustTerminate": true
+        },
+        "__del__": {
+            "args": ["Iterator"],
+            "type": null,
+            "MustTerminate": true
+        }
+    },
+    "type_vars": 1,
+    "extends": "object"
+},
+"Thread": {
+    "extends": "object"
+},
+"LevelType": {
+},
+"type": {
+    "extends": "object"
+},
+"Callable": {
+    "extends": "object"
+},
+"Place": {
+    "functions": {
+        "__eq__": {
+            "args": ["Place", "object"],
+            "type": "__prim__bool"
+        }
+    },
+    "extends": "object"
+},
+"global": {
+    "functions": {
+        "max": {
+            "args": ["object", "object"],
+            "type": "__prim__int",
+            "requires": ["int___unbox__", "list___len__", "list___contains__", "__prim__int___box__"]
+        },
+        "min": {
+            "args": ["object", "object"],
+            "type": "__prim__int",
+            "requires": ["int___unbox__", "list___len__", "list___contains__", "__prim__int___box__"]
+        },
+        "abs": {
+            "args": ["__prim__int"],
+            "type": "__prim__int"
+        }
+    },
+    "methods": {
+        "print": {
+            "args": ["object"],
+            "type": null,
+            "MustTerminate": true
+        }
+    }
+}
+}
diff --git a/src/nagini_translation/sif/resources/references.sil b/src/nagini_translation/sif/resources/references.sil
new file mode 100644
index 000000000..a7d894019
--- /dev/null
+++ b/src/nagini_translation/sif/resources/references.sil
@@ -0,0 +1,10 @@
+/*
+ * Copyright (c) 2019 ETH Zurich
+ * This Source Code Form is subject to the terms of the Mozilla Public
+ * License, v. 2.0. If a copy of the MPL was not distributed with this
+ * file, You can obtain one at http://mozilla.org/MPL/2.0/.
+ */
+
+
+method object___str__(self: Ref) returns (res: Ref)
+    ensures issubtype(typeof(res), str())
\ No newline at end of file
diff --git a/tests/functional/verification/test_print.py b/tests/functional/verification/test_print.py
new file mode 100644
index 000000000..88fb85d05
--- /dev/null
+++ b/tests/functional/verification/test_print.py
@@ -0,0 +1,25 @@
+# Any copyright is dedicated to the Public Domain.
+# http://creativecommons.org/publicdomain/zero/1.0/
+
+from nagini_contracts.contracts import *
+
+
+def foo(i: int) -> None:
+    Requires(LowEvent())
+    print(i)
+
+
+def foo2(i: int) -> None:
+    print(6)
+
+
+class MyObject(object):
+    pass
+
+
+def test(x: int) -> None:
+    Requires(LowEvent())
+    if x > 0:
+      m1 = MyObject()
+    m2 = MyObject()
+    print(str(m2))
diff --git a/tests/sif-true/verification/test_print.py b/tests/sif-true/verification/test_print.py
new file mode 100644
index 000000000..d740e2a4f
--- /dev/null
+++ b/tests/sif-true/verification/test_print.py
@@ -0,0 +1,28 @@
+# Any copyright is dedicated to the Public Domain.
+# http://creativecommons.org/publicdomain/zero/1.0/
+
+from nagini_contracts.contracts import *
+
+
+def foo(i: int) -> None:
+    Requires(LowEvent())
+    #:: ExpectedOutput(call.precondition:assertion.false)
+    print(i)
+
+
+def foo2(i: int) -> None:
+    #:: ExpectedOutput(call.precondition:assertion.false)
+    print(6)
+
+
+class MyObject(object):
+    pass
+
+
+def test(x: int) -> None:
+    Requires(LowEvent())
+    if x > 0:
+      m1 = MyObject()
+    m2 = MyObject()
+    #:: ExpectedOutput(call.precondition:assertion.false)
+    print(str(m2))