Merge pull request #5006 from yumibagge/yb/jbmc-regression-tg-2479

Add regression test for TG-2479

Author: yumibagge

jbmc/regression/jbmc/lambda4/LambdaBasic$If.class

@@ -0,0 +1,37 @@
+public class LambdaBasic {
+
+  private boolean endOnSuccess = true;
+
+  public void testThis(int branch) {
+    boolean endOnSuccess;
+    endOnSuccess = this.endOnSuccess;
+    If boo = () -> {
+      if (endOnSuccess) {
+        return 1;
+      }
+      return 0;
+    };
+
+    int x0 = boo.xInt();
+    // assert successful
+    if (branch == 1) {
+      if (endOnSuccess) {
+        assert x0 == 1;
+      } else {
+        assert x0 == 0;
+      }
+      // assert failed
+    } else {
+      if (endOnSuccess) {
+        assert x0 != 1;
+      } else {
+        assert x0 != 0;
+      }
+    }
+  }
+
+  interface If {
+
+    int xInt();
+  }
+}

jbmc/regression/jbmc/lambda4/LambdaBasic.class

@@ -0,0 +1,13 @@
+CORE
+LambdaBasic.class
+--function LambdaBasic.testThis --property 'java::LambdaBasic.testThis:(I)V.assertion.1' --property 'java::LambdaBasic.testThis:(I)V.assertion.2' --property 'java::LambdaBasic.testThis:(I)V.assertion.3' --property 'java::LambdaBasic.testThis:(I)V.assertion.4'
+line 19 assertion.*SUCCESS$
+line 21 assertion.*SUCCESS$
+line 26 assertion.*FAILURE$
+line 28 assertion.*FAILURE$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+This test is a minimised example reported in TG-2479 and fixed during lambda
+development.