diff --git a/Results/arrays1_true_returnValue != null_returnValueVar == returnValue_True_True_1 b/Results/arrays1_true_returnValue != null_returnValueVar == returnValue_True_True_1
new file mode 100644
index 0000000000000000000000000000000000000000..844c6995b984df66e125f8be1ca31656366832ed
--- /dev/null
+++ b/Results/arrays1_true_returnValue != null_returnValueVar == returnValue_True_True_1	
@@ -0,0 +1,94 @@
+testFile: arrays1
+postCondVoid: true
+postCondRefType: returnValue != null
+postCondPrimType: returnValueVar == returnValue
+ignoreLibMethods: True
+ignoreMainMethod: True
+nrOfUnroll: 1
+erronous mutations detected:
+96 findAndPrintPairs
+93 findAndPrintPairs
+90 findAndPrintPairs
+85 findAndPrintPairs
+82 goodResize
+80 goodResize
+79 goodResize
+78 goodResize
+77 goodResize
+76 goodResize
+75 goodResize
+74 goodResize
+71 goodResize
+68 goodResize
+67 goodResize
+65 goodResize
+60 badResize
+59 badResize
+58 badResize
+57 badResize
+55 badResize
+52 badResize
+49 badResize
+48 badResize
+46 badResize
+39 findMin
+38 findMin
+36 findMin
+35 findMin
+34 findMin
+33 findMin
+30 findMin
+28 findMin
+24 findMin
+217 bubblesort
+217 isAscending
+215 isAscending
+214 isAscending
+213 isAscending
+212 isAscending
+211 isAscending
+210 isAscending
+209 isAscending
+208 isAscending
+207 isAscending
+206 isAscending
+203 isAscending
+201 isAscending
+196 isAscending
+192 bubblesort
+192 isAscending
+191 isAscending
+189 isAscending
+188 isAscending
+187 bubblesort
+187 isAscending
+186 bubblesort
+186 isAscending
+185 isAscending
+184 bubblesort
+184 isAscending
+173 bubblesort
+170 bubblesort
+167 bubblesort
+164 bubblesort
+156 bubblesort
+153 bubblesort
+149 bubblesort
+147 bubblesort
+137 bubblesort
+134 bubblesort
+132 bubblesort
+130 bubblesort
+129 bubblesort
+128 bubblesort
+126 bubblesort
+125 bubblesort
+124 bubblesort
+121 bubblesort
+120 bubblesort
+114 bubblesort
+112 bubblesort
+109 bubblesort
+107 bubblesort
+Total number of mutants: 217
+Number of mutants in which we found an error: 79
\ No newline at end of file
diff --git a/Verifier.hs b/Verifier.hs
index b9114cdc3a99519b2517dcf6d04ca674458f5db7..73f6e84e081f52850b603f625358e288360ce015 100644
--- a/Verifier.hs
+++ b/Verifier.hs
@@ -96,14 +96,17 @@ expAssertAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQual
                                             ArrayIndex e _ -> foldExp expAssertAlgebra e env decls
     fExpName name env decls      = do
                                     symbol <- mkStringSymbol (prettyPrint name)
-                                    case lookupType decls env name of
-                                        PrimType BooleanT    -> mkBoolVar symbol
-                                        PrimType FloatT      -> mkRealVar symbol
-                                        PrimType DoubleT     -> mkRealVar symbol
-                                        PrimType IntT        -> mkIntVar symbol
-                                        RefType _            -> mkIntVar symbol
+                                    case prettyPrint name of
                                         -- For now, we assume library methods return ints. Fixing this would require type information of library methods.
-                                        t                           -> if ignoreLibMethods then mkStringSymbol "libMethodCall" >>= mkIntVar else error ("Verifier: Type of " ++ prettyPrint name ++ " unknown or not implemented: " ++ show t)
+                                        '$':_   -> if ignoreLibMethods then mkStringSymbol "libMethodCall" >>= mkIntVar else error "introduced variable in WLP expression"
+                                        -- If we're not dealing with library methods, we should be able to get the type from the type environment
+                                        _       -> case lookupType decls env name of
+                                                        PrimType BooleanT    -> mkBoolVar symbol
+                                                        PrimType FloatT      -> mkRealVar symbol
+                                                        PrimType DoubleT     -> mkRealVar symbol
+                                                        PrimType IntT        -> mkIntVar symbol
+                                                        RefType _            -> mkIntVar symbol
+                                                        t                           -> error ("Verifier: Type of " ++ prettyPrint name ++ " unknown or not implemented: " ++ show t)
     fPostIncrement = undefined
     fPostDecrement = undefined
     fPreIncrement = undefined