diff --git a/src/LogicIR/Backend/Test.hs b/src/LogicIR/Backend/Test.hs
index 9d5c8764124ff76d5ce4ae41bc7625e1659b53b8..facb844541402157669f83f89de31655220b0f94 100644
--- a/src/LogicIR/Backend/Test.hs
+++ b/src/LogicIR/Backend/Test.hs
@@ -44,9 +44,6 @@ testEquality 0 e1 e2 = do
 testEquality n e1 e2 = do
     (r,m1,m2) <- test e1 e2
     if not r then do 
-        putStrLn $ show r
-        putStrLn $ show m1
-        putStrLn $ show m2
         return (False, (m1, m2))
     else do
         (rs, model) <- testEquality (n-1) e1 e2
@@ -59,11 +56,14 @@ testEquality n e1 e2 = do
 testLExpr :: LExpr -> IO (LConst, EvalInfo)
 testLExpr e = do 
     let vs@(regularVs, (arrayVs, arrayOpVs), quantVs) = findVariables e
-    primitivesModel  <- generateModel regularVs
+    let isNullExprs   = filter sIsnullExpr arrayOpVs
+    primitivesModel  <- generateModel (regularVs ++ isNullExprs)
     arrayModel       <- generateArrayModel arrayVs
     testResult       <- testModel e (primitivesModel, arrayModel, quantVs)
     let evalInfo      = (primitivesModel, arrayModel, quantVs)
     return (testResult, evalInfo)
+    where sIsnullExpr (LIsnull _) = True
+          sIsnullExpr _           = False
 
 testModel :: LExpr -> EvalInfo -> IO LConst
 testModel e evalInfo = do
@@ -120,9 +120,13 @@ subst   q@(LQuant qop v domain e) evalInfo = do
       q
     else
       LConst $ CBool $ op $ map fromJust results
-subst (LIsnull v)  (_,arrayModel,_) = LConst (CBool (0 == length (tr arrayModel v)))
 subst (LLen    v)  (_,arrayModel,_) = LConst (CInt (length (tr arrayModel v)))
 subst v (model,_,_)                 = fromMaybe v (fmap snd $ find (\(old,new) -> v == old) model)
+-- Note that firstly,  LIsnull can only be applied to arrays since ints/bools cannot be null in Java,
+--           secondly, LIsnull is not substituted based on the actual value of the array in the
+--                     ArrayModel. Instead, it's just a random bool that is present in the primitives model.
+--                     This is because otherwise, the evaluation of an LExpr should be changed drastically.
+--                     After all, How do you evaluate a[0] or a.length if a == null...
 
 -- Returns, given a domain LExpr that concerns a certain Var, all
 -- Ints that fall in that domain.
@@ -136,8 +140,6 @@ evalQuantifier v domain e (m1,m2,quantVs) = do
           getResult newM1 = do
               let newEvalInfo = (newM1,m2,quantVs)
               let newDomain = applyModel domain newEvalInfo
-              --let !x = unsafePerformIO $ putStrLn $ prettyLExpr domain
-              --let !x = unsafePerformIO $ putStrLn $ prettyLExpr newDomain ++ "\n"
               if evalPossible newDomain then
                   if isTrue newDomain then do
                       let newE = applyModel e newEvalInfo
@@ -184,11 +186,8 @@ generateModelEntry e@(LVar (Var (TPrim t) _)) = do
     generatePrimitive t >>= \v -> return (e, v)
 generateModelEntry e@(LIsnull (Var (TArray _) _)) = do
     generatePrimitive PBool >>= \v -> return (e, v)
-generateModelEntry e = do
+generateModelEntry e =
     error $ "Cannot generate model entry for " ++ show e
-    return (e, e)
---generateModelEntry e@(LArray (Var (TArray (TPrim t)) _) _) = do
-    --generatePrimitive t >>= \v -> return (e, v)
 
 generatePrimitive :: Primitive -> IO LExpr
 generatePrimitive t = generatePrimitiveWithBounds t (bounds t)
diff --git a/src/SimpleFormulaChecker.hs b/src/SimpleFormulaChecker.hs
index f9439f53d157e97f7961d494a7b1a17447968f54..393dfb4ade5509f1e7cb7aa30dbbb628d90bb864 100644
--- a/src/SimpleFormulaChecker.hs
+++ b/src/SimpleFormulaChecker.hs
@@ -245,11 +245,6 @@ testSpec method1@(_, name1) method2@(_, name2) n = do
     putStrLn "\n----POST---"
     let (lExpr1, lExpr2) = methodDefToLExpr m1 m2 "post"
     (postAns, counterModel) <- testEquality n lExpr1 lExpr2
-
-    appendFile "results.txt" (name1 ++ ", " ++ name2 ++ "\n")
-    appendFile "results.txt" ("Pre  condition equality counter model: " ++ (show counterModel) ++ "\n")
-    appendFile "results.txt" ("Post condition equality counter model: " ++ (show counterModel) ++ "\n")
-
     return $ preAns && postAns
 
 test9 = testSpec (edslSrc, "swap_spec1") (edslSrc, "swap_spec4") 1000
diff --git a/test/TIRTest.hs b/test/TIRTest.hs
index 8e16ff60c60be2bbe8f1b6e6200ea03dbeb7c29a..448e8921f5c2ea0bb75baebb3e98bdae2e81dbcf 100644
--- a/test/TIRTest.hs
+++ b/test/TIRTest.hs
@@ -23,8 +23,8 @@ testingModuleTests =
   , (neq "test1_" "test2" 100)
   , (neq "null1" "null2" 100)
   , (neq "swap_spec1" "swap_spec3" 100)
-  , (neq "swap_spec1" "swap_spec4" 100) --9
-  , (neq "null3" "test2" 1000) --10
+  , (neq "swap_spec1" "swap_spec4" 100)
+  , (neq "null3" "test2" 1000)
   , (neq "sorted1" "test2" 100)
   , (neq "sorted1" "sorted2" 500)
   , (neq "sorted1" "sorted3" 100)