Add simpler case_distinction tests

tests/regression/46-apron2/64-case_distinction_with_ghosts.c

@@ -19,7 +19,7 @@ void* inc()
     __VERIFIER_atomic_end();
 
     __VERIFIER_atomic_begin();
-    assert(g != 1 || x >= 42);
+    assert(g != 1 || x >= 42); // TODO
     __VERIFIER_atomic_end();
   }
 
@@ -34,6 +34,6 @@ int main()
   g = 1; x = 42;
   __VERIFIER_atomic_end();
 
-  assert(x >= 42);
+  assert(x >= 42); // TODO
   return 0;
 }

tests/regression/46-apron2/65-case_distinction_with_ghosts-2.c

@@ -0,0 +1,30 @@
+// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set sem.int.signed_overflow assume_none
+#include <pthread.h>
+#include <assert.h>
+
+extern int  __VERIFIER_nondet_int();
+extern void __VERIFIER_atomic_begin();
+extern void __VERIFIER_atomic_end();
+
+int x = 0;
+int g = 0;
+
+void* inc()
+{
+  __VERIFIER_atomic_begin();
+  assert(g != 1 || x >= 42); // TODO
+  __VERIFIER_atomic_end();
+  return 0;
+}
+
+int main()
+{
+  pthread_t tid;
+  pthread_create(&tid, 0, inc, 0);
+  __VERIFIER_atomic_begin();
+  g = 1; x = 42;
+  __VERIFIER_atomic_end();
+
+  assert(x >= 42); // TODO
+  return 0;
+}

tests/regression/46-apron2/66-case_distinction_with_ghosts-3.c

@@ -0,0 +1,30 @@
+// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set sem.int.signed_overflow assume_none
+#include <pthread.h>
+#include <assert.h>
+
+extern int  __VERIFIER_nondet_int();
+extern void __VERIFIER_atomic_begin();
+extern void __VERIFIER_atomic_end();
+
+int x = 0;
+int g = 0;
+
+void* inc()
+{
+  // x = 10; // TODO: what is this?
+
+  __VERIFIER_atomic_begin();
+  assert(g != 1 || x >= 42); // TODO
+  __VERIFIER_atomic_end();
+  return 0;
+}
+
+int main()
+{
+  pthread_t tid;
+  pthread_create(&tid, 0, inc, 0);
+  __VERIFIER_atomic_begin();
+  g = 1; x = 42;
+  __VERIFIER_atomic_end();
+  return 0;
+}