diff --git a/src/ModelParser/Lexer.x b/src/ModelParser/Lexer.x
index 355f667fa50d46380f60ad9d4fba4e699191811d..0a26bc804180013b3b3a5306b3ae0ef2b76cff3f 100644
--- a/src/ModelParser/Lexer.x
+++ b/src/ModelParser/Lexer.x
@@ -28,7 +28,7 @@ tokens :-
     "false"     { \s -> Tbool False }
     "#x"$value+ { \s -> Tvalue (parseHex s) }
     $num+       { \s -> Tvalue (parseDec s) }
-    $ident+     { \s -> Tident s }    
+    $ident+     { \s -> Tident s }
 {
 
 data Token = Tarrow
diff --git a/src/SimpleFormulaChecker.hs b/src/SimpleFormulaChecker.hs
index 017b9460a7f8c71a96d887013518a95498f1df5e..17dd79acded3559316f12d26d7173a109ae978d5 100644
--- a/src/SimpleFormulaChecker.hs
+++ b/src/SimpleFormulaChecker.hs
@@ -98,9 +98,33 @@ showRelevantModel model = do
         prettyModelVal :: (String, ModelVal) -> String
         prettyModelVal (k, BoolVal b) = k ++ " = " ++ if b then "true" else "false"
         prettyModelVal (k, IntVal n) = k ++ " = " ++ show n
-        prettyModelVal (k, ArrayFunc a) = k ++ " = " ++ show n -- TODO: lookup (k ++ "?length") and (k ++ "?null") and handle all cases
-            where n = a -- TODO: properly try to convert to a list
-        prettyModelVal (k, v) = error $ k ++ " = UNIMPLEMENTED " ++ show v        
+        prettyModelVal (k, ArrayFunc a) = k ++ " = " ++ final ++ "       " ++ show (aNull, aLength, arrKv, validArr, elseVal)
+            where (BoolVal aNull) = M.findWithDefault (BoolVal False) (k ++ "?null") modelClean
+                  (IntVal aLength) = M.findWithDefault (IntVal (-1)) (k ++ "?length") modelClean
+                  [InstElse elseVal] = filter (not . isInst) a
+                  arrKv = sort (map (\(InstInt k v) -> (k, v)) (filter isInst a))
+                  isInst (InstInt _ _) = True
+                  isInst _ = False
+                  validArr = isValidArray 0 arrKv
+                  -- TODO: this does not appear to be correct yet
+                  final = if aNull
+                             then if (aLength /= -1) || (length arrKv /= 0)
+                                     then "1: INVALID"
+                                     else "2: null"
+                             else if validArr
+                                     then if length arrKv == aLength
+                                             then "3: " ++ show (map snd arrKv)
+                                             else "4: INVALID"
+                                     else if aLength /= -1
+                                             then "5: " ++ show (take aLength (repeat elseVal))
+                                             else "6: INVALID"
+
+                  isValidArray :: Int -> [(Int, Int)] -> Bool
+                  isValidArray n [] = False
+                  isValidArray n ((i, _) : xs) = if n == i
+                                                    then isValidArray (n + 1) xs
+                                                    else False
+        prettyModelVal (k, v) = error $ k ++ " = UNIMPLEMENTED " ++ show v
         -- Remove all occurrences of ArrayRef and ArrayAsConst for easier processing later, also does type casting
         modelCleanFunc :: ModelVal -> ModelVal
         modelCleanFunc (BoolVal b) = BoolVal b
@@ -137,7 +161,6 @@ showRelevantModel model = do
                          IntVal _ -> True
                          _ -> False
 
-
 -- Determine the equality of two method's pre/post conditions.
 determineFormulaEq :: MethodDef -> MethodDef -> String -> IO ()
 determineFormulaEq m1@(decls1, mbody1, env1) m2@(decls2, mbody2, env2) name = do