- Fixed bug that caused extractExpr to crash when it tried to fetch all pre /...

- Fixed bug that caused extractExpr to crash when it tried to fetch all pre / post conditions of a method that doesn’t have any.
- Increased the number of iterations in the tenth LogicIR.Backend.Test test.

examples/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java

@@ -14,7 +14,7 @@ public class Main {
     public static void quickcheck_test2(int[] b) {
         pre(~(-a * c) == (79 & 41));
         pre(a > 0);
-        pre(forall(b, i -> b[i] >= -10)); // note the >=, whereas test1 has >.
+        pre(forall(b, i -> b[i] >= -10)); // note the >=, whereas quickcheck_test1 has >.
     }
 
     public static int simple_eval1() {

src/SimpleFormulaChecker.hs

@@ -71,6 +71,7 @@ getMethodCalls (_, StmtBlock (Block bs), _) name = mapMaybe extractMethodInv bs
 extractExpr :: [MethodInvocation] -> Exp
 extractExpr call = combineExprs $ map (\(MethodCall (Name [Ident _]) [a]) -> a) call
     where combineExprs :: [Exp] -> Exp
+          combineExprs []  = Lit $ Boolean True -- If the expression is empty, just return True.
           combineExprs [e] = e
           combineExprs (e:es) = BinOp e CAnd (combineExprs es)
 
@@ -233,7 +234,7 @@ methodDefToLExpr m1@(decls1, _, env1) m2@(decls2, _, env2) name = do
     -- preprocess "a == null" to "isNull(a)"
     let (lExpr1, lExpr2) = (lExprPreprocessNull lExpr1', lExprPreprocessNull lExpr2')
     (lExpr1, lExpr2)
-    where extractCond m n = extractExpr $ getMethodCalls m n
+        where extractCond m n = extractExpr $ getMethodCalls m n
 
 testSpec :: (FilePath, String) -> (FilePath, String) -> Int -> IO Bool
 testSpec method1@(_, name1) method2@(_, name2) n = do

test/TIRTest.hs

@@ -24,7 +24,7 @@ testingModuleTests =
   , (neq "null1" "null2" 10)
   , (neq "swap_spec1" "swap_spec3" 100)
   , (neq "swap_spec1" "swap_spec4" 100)
-  , (neq "null3" "test2" 10)
+  , (neq "null3" "test2" 100)
   , (neq "sorted1" "test2" 10)
   , (neq "sorted1" "sorted2" 1000)
   , (neq "sorted1" "sorted3" 1000)