diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml
index 351b59d..ffea94f 100644
--- a/.github/workflows/ci.yaml
+++ b/.github/workflows/ci.yaml
@@ -19,7 +19,7 @@ jobs:
 
       - name: Download and install Isabelle
         run: |
-          wget --quiet https://isabelle.in.tum.de/dist/Isabelle2022_linux.tar.gz
+          wget --quiet https://isabelle.in.tum.de/website-Isabelle2022/dist/Isabelle2022_linux.tar.gz
           tar -xf Isabelle2022_linux.tar.gz
           rm Isabelle2022_linux.tar.gz
           mv Isabelle2022 isabelle_dir
diff --git a/BoogieLang/Lang.thy b/BoogieLang/Lang.thy
index d0db732..b799431 100644
--- a/BoogieLang/Lang.thy
+++ b/BoogieLang/Lang.thy
@@ -11,7 +11,7 @@ type_synonym pname = string (* procedure name *)
 datatype lit =  LBool bool  | LInt int | LReal real
 
 datatype binop = Eq | Neq | Add | Sub | Mul | Div | RealDiv | Mod | Lt | Le | Gt | Ge | And | Or | Imp | Iff
-datatype unop = Not | UMinus
+datatype unop = Not | UMinus | IntToReal
 
 datatype prim_ty 
  = TBool | TInt | TReal
diff --git a/BoogieLang/PassificationML.thy b/BoogieLang/PassificationML.thy
index 27c8802..9ecc06c 100644
--- a/BoogieLang/PassificationML.thy
+++ b/BoogieLang/PassificationML.thy
@@ -1,5 +1,5 @@
 theory PassificationML
-imports Boogie_Lang.Semantics HelperML Passification
+imports Semantics HelperML Passification
 begin
 
 ML \<open>
diff --git a/BoogieLang/Semantics.thy b/BoogieLang/Semantics.thy
index 81e3c6f..eeef2f3 100644
--- a/BoogieLang/Semantics.thy
+++ b/BoogieLang/Semantics.thy
@@ -367,10 +367,16 @@ fun unop_minus :: "lit \<rightharpoonup> lit"
   | "unop_minus (LReal r) = Some (LReal (-r))"
   | "unop_minus _ = None"
 
+fun unop_int_to_real :: "lit \<rightharpoonup> lit"
+  where 
+    "unop_int_to_real (LInt i) = Some (LReal (real_of_int i))"
+  | "unop_int_to_real _ = None"
+
 fun unop_eval :: "unop \<Rightarrow> lit \<rightharpoonup> lit"
   where 
    "unop_eval Not v = unop_not v"
  | "unop_eval UMinus v = unop_minus v"
+ | "unop_eval IntToReal v = unop_int_to_real v"
 
 fun unop_eval_val :: "unop \<Rightarrow> 'a val \<rightharpoonup> 'a val"
   where
diff --git a/BoogieLang/Typing.thy b/BoogieLang/Typing.thy
index b756817..d17985d 100644
--- a/BoogieLang/Typing.thy
+++ b/BoogieLang/Typing.thy
@@ -16,6 +16,9 @@ fun unop_type :: "unop \<Rightarrow> prim_ty \<Rightarrow> prim_ty option"
   | "unop_type Not TInt = None"
   | "unop_type Not TReal = None"
   | "unop_type Not TBool = Some TBool"
+  | "unop_type IntToReal TInt = Some TReal"
+  | "unop_type IntToReal TReal = None"
+  | "unop_type IntToReal TBool = None"
 
 primrec binop_type :: "binop \<Rightarrow> ((prim_ty \<times> prim_ty) set \<times> prim_ty) option"
   where