Exclude programs with flapping timeouts in integration sets

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@42558 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c

test/test-sets/integration-arrayAbstraction-predicate.xml

@@ -25,6 +25,7 @@ SPDX-License-Identifier: Apache-2.0
     <propertyfile>../programs/benchmarks/properties/unreach-call.prp</propertyfile>
     <!-- SV-Comp files assume that malloc always succeeds -->
     <option name="-setprop">cpa.predicate.memoryAllocationsAlwaysSucceed=true</option>
+    <exclude>../programs/benchmarks/array-fpi/modnf.yml</exclude> <!-- flapping timeout -->
   </tasks>
   <tasks>
     <includesfile>../programs/benchmarks/ReachSafety-Floats.set</includesfile>
@@ -48,6 +49,7 @@ SPDX-License-Identifier: Apache-2.0
     <propertyfile>../programs/benchmarks/properties/unreach-call.prp</propertyfile>
     <!-- SV-Comp files assume that malloc always succeeds -->
     <option name="-setprop">cpa.predicate.memoryAllocationsAlwaysSucceed=true</option>
+    <exclude>../programs/benchmarks/loops/vogal-2.yml</exclude> <!-- flapping timeout -->
     <exclude>../programs/benchmarks/nla-digbench-scaling/cohendiv-ll_valuebound2.yml</exclude> <!-- flapping timeout -->
     <exclude>../programs/benchmarks/nla-digbench-scaling/geo3-ll_valuebound2.yml</exclude> <!-- flapping timeout -->
     <exclude>../programs/benchmarks/nla-digbench-scaling/hard2_unwindbound5.yml</exclude> <!-- flapping timeout -->

test/test-sets/integration-bdd.xml

@@ -75,6 +75,7 @@ SPDX-License-Identifier: Apache-2.0
     <exclude>../programs/benchmarks/loops/*string*</exclude>
     <exclude>../programs/benchmarks/nla-digbench-scaling/*</exclude> <!-- only FALSE results due to missing multiplication support in BDD analysis -->
     <exclude>../programs/benchmarks/loop-invgen/*</exclude> <!-- mostly OOM/StackOverflow -->
+    <exclude>../programs/benchmarks/loops-crafted-1/mono-crafted_13.yml</exclude> <!-- flapping timeout / wrong alarm -->
     <exclude>../programs/benchmarks/loops-crafted-1/theatreSquare.yml</exclude> <!-- flapping OOM/StackOverflow -->
   </tasks>
 </benchmark>

test/test-sets/integration-induction.xml

@@ -81,6 +81,7 @@ SPDX-License-Identifier: Apache-2.0
     <exclude>../programs/benchmarks/loops/sum01-2.yml</exclude> <!-- flapping timeouts -->
     <exclude>../programs/benchmarks/loops/vogal-1.yml</exclude> <!-- flapping timeout -->
     <exclude>../programs/benchmarks/loop-new/gauss_sum.i.*-reducer.yml</exclude> <!-- flapping timeouts -->
+    <exclude>../programs/benchmarks/nla-digbench-scaling/bresenham-ll_valuebound1.yml</exclude> <!-- flapping timeout -->
     <exclude>../programs/benchmarks/nla-digbench-scaling/bresenham-ll_unwindbound2.yml</exclude> <!-- flapping timeout -->
     <exclude>../programs/benchmarks/nla-digbench-scaling/cohencu-ll_unwindbound10.yml</exclude> <!-- flapping timeout -->
     <exclude>../programs/benchmarks/nla-digbench-scaling/cohendiv-ll_unwindbound2.yml</exclude> <!-- flapping timeout -->
@@ -94,12 +95,14 @@ SPDX-License-Identifier: Apache-2.0
     <exclude>../programs/benchmarks/nla-digbench-scaling/geo3-ll_valuebound5.yml</exclude> <!-- flapping timeout -->
     <exclude>../programs/benchmarks/nla-digbench-scaling/geo3-ll_valuebound10.yml</exclude> <!-- flapping timeout -->
     <exclude>../programs/benchmarks/nla-digbench-scaling/hard2_unwindbound20.yml</exclude> <!-- flapping timeout -->
+    <exclude>../programs/benchmarks/nla-digbench-scaling/hard2_valuebound50.yml</exclude> <!-- flapping timeout -->
     <exclude>../programs/benchmarks/nla-digbench-scaling/mannadiv_unwindbound20.yml</exclude> <!-- flapping timeout -->
     <exclude>../programs/benchmarks/nla-digbench-scaling/prod4br-ll_valuebound1.yml</exclude> <!-- flapping timeout -->
     <exclude>../programs/benchmarks/nla-digbench-scaling/prodbin-ll_valuebound1.yml</exclude> <!-- flapping timeout -->
     <exclude>../programs/benchmarks/nla-digbench-scaling/prodbin-ll_valuebound5.yml</exclude> <!-- flapping timeout -->
     <exclude>../programs/benchmarks/nla-digbench-scaling/prodbin-ll_valuebound10.yml</exclude> <!-- flapping timeout -->
     <exclude>../programs/benchmarks/nla-digbench-scaling/prodbin-ll_valuebound20.yml</exclude> <!-- flapping timeout -->
+    <exclude>../programs/benchmarks/nla-digbench-scaling/prodbin-ll_valuebound50.yml</exclude> <!-- flapping timeout -->
     <exclude>../programs/benchmarks/nla-digbench-scaling/ps4-ll_unwindbound20.yml</exclude> <!-- flapping timeout -->
     <!-- SV-Comp files assume that malloc always succeeds -->
     <option name="-setprop">cpa.predicate.memoryAllocationsAlwaysSucceed=true</option>

test/test-sets/integration-ismc.xml

@@ -38,6 +38,7 @@ SPDX-License-Identifier: Apache-2.0
     <propertyfile>../programs/benchmarks/properties/unreach-call.prp</propertyfile>
     <!-- SV-Comp files assume that malloc always succeeds -->
     <option name="-setprop">cpa.predicate.memoryAllocationsAlwaysSucceed=true</option>
+    <exclude>../programs/benchmarks/bitvectors/s3_srvr_1a.BV.c.cil.yml</exclude> <!-- flapping timeout -->
   </tasks>
   <tasks>
     <includesfile>../programs/benchmarks/ReachSafety-Floats.set</includesfile>
@@ -51,6 +52,7 @@ SPDX-License-Identifier: Apache-2.0
     <exclude>../programs/benchmarks/floats-cbmc-regression/float4.yml</exclude> <!-- flapping timeout -->
     <exclude>../programs/benchmarks/floats-cdfpl/square_1.yml</exclude> <!-- flapping timeout -->
     <exclude>../programs/benchmarks/floats-cdfpl/sine_3.yml</exclude> <!-- flapping timeout -->
+    <exclude>../programs/benchmarks/float-newlib/double_req_bl_0530b.yml</exclude> <!-- flapping timeout -->
     <exclude>../programs/benchmarks/float-newlib/double_req_bl_0550a.yml</exclude> <!-- flapping timeout -->
     <exclude>../programs/benchmarks/loop-floats-scientific-comp/loop3.yml</exclude> <!-- flapping timeout -->
   </tasks>
@@ -65,6 +67,9 @@ SPDX-License-Identifier: Apache-2.0
     <propertyfile>../programs/benchmarks/properties/unreach-call.prp</propertyfile>
     <!-- SV-Comp files assume that malloc always succeeds -->
     <option name="-setprop">cpa.predicate.memoryAllocationsAlwaysSucceed=true</option>
+    <exclude>../programs/benchmarks/ldv-sets/test_mutex.yml</exclude> <!-- flapping timeout -->
+    <exclude>../programs/benchmarks/list-ext2-properties/simple_search_value-2.yml</exclude> <!-- flapping timeout -->
+    <exclude>../programs/benchmarks/list-ext3-properties/dll_circular_traversal-2.yml</exclude> <!-- flapping timeout -->
   </tasks>
   <tasks>
     <includesfile>../programs/benchmarks/ReachSafety-Loops.set</includesfile>
@@ -106,5 +111,6 @@ SPDX-License-Identifier: Apache-2.0
     <option name="-setprop">cpa.predicate.memoryAllocationsAlwaysSucceed=true</option>
     <exclude>../programs/benchmarks/ldv-linux-3.0/module_get_put-drivers-isdn-mISDN-mISDN_core.ko.cil.out.yml</exclude> <!-- flapping timeout -->
     <exclude>../programs/benchmarks/ldv-linux-3.4-simple/43_1a_cilled_ok_nondet_linux-43_1a-drivers--rtc--rtc-rs5c348.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.yml</exclude> <!-- flapping timeout -->
+    <exclude>../programs/benchmarks/ldv-linux-3.4-simple/43_1a_cilled_ok_nondet_linux-43_1a-drivers--power--max8903_charger.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.yml</exclude> <!-- flapping timeout / out of native memory -->
   </tasks>
 </benchmark>

test/test-sets/integration-ldv-unsafes.xml

@@ -31,11 +31,13 @@ SPDX-License-Identifier: Apache-2.0
     <include>../programs/ldv-benchmarks/unsafes/*/*/*.yml</include>
     <exclude>../programs/ldv-benchmarks/validator/v0.7/linux-stable-90a4845-110_1a-drivers--char--ipmi--ipmi_si.ko-ldv_main0.cil.out.yml</exclude> <!-- flapping timeout / wrong result -->
     <exclude>../programs/ldv-benchmarks/unsafes/08_1a/linux-3.12-rc1/linux-3.12-rc1.tar.xz-08_1a-fs--nfs--nfs.ko-ldv_main5.cil.out.yml</exclude> <!-- flapping timeout -->
+    <exclude>../programs/ldv-benchmarks/unsafes/08_1a/linux-3.16-rc1/linux-3.16-rc1.tar.xz-08_1a-drivers--staging--dgrp--dgrp.ko-ldv_main3.cil.out.yml</exclude> <!-- flapping timeout -->
     <exclude>../programs/ldv-benchmarks/unsafes/08_1a/linux-3.16-rc1/linux-3.16-rc1.tar.xz-08_1a-sound--pci--hda--snd-hda-codec.ko-ldv_main0.cil.out.yml</exclude> <!-- flapping timeout -->
     <exclude>../programs/ldv-benchmarks/unsafes/08_1a/linux-3.16-rc1/linux-3.16-rc1.tar.xz-08_1a-drivers--fmc--fmc-chardev.ko-ldv_main0.cil.out.yml</exclude> <!-- flapping timeout -->
     <exclude>../programs/ldv-benchmarks/unsafes/08_1a/linux-3.16-rc1/linux-3.16-rc1.tar.xz-08_1a-drivers--target--target_core_mod.ko-ldv_main0.cil.out.yml</exclude> <!-- flapping timeout/error -->
     <exclude>../programs/ldv-benchmarks/unsafes/08_1a/linux-3.16-rc1/linux-3.16-rc1.tar.xz-08_1a-net--sunrpc--sunrpc.ko-ldv_main18.cil.out.yml</exclude> <!-- flapping timeout -->
     <exclude>../programs/ldv-benchmarks/unsafes/10_1a/linux-3.12-rc1/linux-3.12-rc1.tar.xz-10_1a-drivers--net--wireless--iwlwifi--iwlwifi.ko-ldv_main9.cil.out.yml</exclude> <!-- flapping timeout -->
+    <exclude>../programs/ldv-benchmarks/unsafes/39_7a/linux-3.12-rc1/linux-3.12-rc1.tar.xz-39_7a-net--irda--irda.ko-ldv_main19.cil.out.yml</exclude> <!-- flapping timeout -->
     <exclude>../programs/ldv-benchmarks/unsafes/129_1a/linux-3.12-rc1/fs--ext3--ext3.ko-ldv_main17.cil.out.yml</exclude> <!-- flapping timeout -->
     <exclude>../programs/ldv-benchmarks/unsafes/130_7a/linux-3.16-rc1/linux-3.16-rc1.tar.xz-130_7a-drivers--block--virtio_blk.ko-ldv_main0.cil.out.yml</exclude> <!-- flapping timeout -->
     <exclude>../programs/ldv-benchmarks/unsafes/130_7a/linux-3.16-rc1/linux-3.16-rc1.tar.xz-130_7a-drivers--net--ethernet--qlogic--netxen--netxen_nic.ko-ldv_main3.cil.out.yml</exclude> <!-- flapping timeout -->

test/test-sets/integration-nightly-smg.xml

@@ -46,6 +46,7 @@ SPDX-License-Identifier: Apache-2.0
   <tasks name="MemSafety-Heap">
     <includesfile>../programs/benchmarks/MemSafety-Heap.set</includesfile>
     <propertyfile>../programs/benchmarks/properties/valid-memsafety.prp</propertyfile>
+    <exclude>../programs/benchmarks/ldv-memsafety/ArraysOfVariableLength2.yml</exclude> <!-- flapping timeout -->
   </tasks>
   <tasks name="MemSafety-LinkedLists">
     <includesfile>../programs/benchmarks/MemSafety-LinkedLists.set</includesfile>

test/test-sets/integration-nightly-smg2-CEGAR.xml

@@ -38,6 +38,8 @@ SPDX-License-Identifier: Apache-2.0
   <tasks name="ReachSafety-ECA">
     <includesfile>../programs/benchmarks/ReachSafety-ECA.set</includesfile>
     <propertyfile>../programs/benchmarks/properties/unreach-call.prp</propertyfile>
+    <exclude>../programs/benchmarks/eca-rers2012/Problem09_label22.yml</exclude> <!-- flapping timeout / exception -->
+    <exclude>../programs/benchmarks/eca-rers2012/Problem12_label50.yml</exclude> <!-- flapping timeout -->
   </tasks>
   <tasks name="ReachSafety-Floats">
     <includesfile>../programs/benchmarks/ReachSafety-Floats.set</includesfile>

test/test-sets/integration-nightly-smg2.xml

@@ -38,6 +38,7 @@ SPDX-License-Identifier: Apache-2.0
   <tasks name="ReachSafety-ECA">
     <includesfile>../programs/benchmarks/ReachSafety-ECA.set</includesfile>
     <propertyfile>../programs/benchmarks/properties/unreach-call.prp</propertyfile>
+    <exclude>../programs/benchmarks/eca-rers2012/Problem12_label50.yml</exclude> <!-- flapping timeout -->
   </tasks>
   <tasks name="ReachSafety-Floats">
     <includesfile>../programs/benchmarks/ReachSafety-Floats.set</includesfile>

test/test-sets/integration-pdr.xml

@@ -76,8 +76,10 @@ SPDX-License-Identifier: Apache-2.0
     <exclude>../programs/benchmarks/loop-lit/*</exclude> <!-- mostly timeouts -->
     <exclude>../programs/benchmarks/loop-invgen/apache-get-tag.i.*-reducer.yml</exclude> <!-- flapping timeout -->
     <exclude>../programs/benchmarks/loop-invgen/id_build.yml</exclude> <!-- flapping timeout -->
+    <exclude>../programs/benchmarks/loop-invgen/id_build.i.v+lhb-reducer.yml</exclude> <!-- flapping timeout -->
     <exclude>../programs/benchmarks/loop-invariants/linear-inequality-inv-b.yml</exclude> <!-- flapping timeout -->
     <exclude>../programs/benchmarks/loops-crafted-1/*</exclude> <!-- only timeouts -->
+    <exclude>../programs/benchmarks/loop-zilu/benchmark18_conjunctive.yml</exclude> <!-- only timeouts -->
     <exclude>../programs/benchmarks/nla-digbench/*</exclude> <!-- only timeouts -->
     <exclude>../programs/benchmarks/nla-digbench-scaling/*</exclude> <!-- mostly timeouts -->
 

test/test-sets/integration-predicate-bitprecise.xml

@@ -79,8 +79,9 @@ SPDX-License-Identifier: Apache-2.0
     <exclude>../programs/benchmarks/seq-mthreaded/pals_STARTPALS_ActiveStandby.5.ufo.BOUNDED-10.pals.yml</exclude> <!-- flapping timeout -->
     <exclude>../programs/benchmarks/seq-mthreaded/pals_STARTPALS_Triplicated.ufo.UNBOUNDED.pals.yml</exclude> <!-- flapping timeout -->
     <exclude>../programs/benchmarks/seq-mthreaded/pals_floodmax.4.1.ufo.BOUNDED-8.pals.yml</exclude> <!-- flapping timeout -->
-    <exclude>../programs/benchmarks/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.UNBOUNDED.pals.c.v+cfa-reducer.yml</exclude> <!-- flapping timeout -->
     <exclude>../programs/benchmarks/seq-mthreaded-reduced/pals_floodmax.5.2.ufo.BOUNDED-10.pals.c.v+cfa-reducer.yml</exclude> <!-- flapping timeout -->
+    <exclude>../programs/benchmarks/seq-mthreaded-reduced/pals_lcr-var-start-time.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.yml</exclude> <!-- flapping timeout -->
+    <exclude>../programs/benchmarks/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.UNBOUNDED.pals.c.v+cfa-reducer.yml</exclude> <!-- flapping timeout -->
     <exclude>../programs/benchmarks/seq-mthreaded-reduced/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.c.v+cfa-reducer.yml</exclude> <!-- flapping timeout -->
     <exclude>../programs/benchmarks/seq-mthreaded-reduced/pals_opt-floodmax.4.3.ufo.UNBOUNDED.pals.c.v+cfa-reducer.yml</exclude> <!-- flapping timeout -->
     <exclude>../programs/benchmarks/systemc/toy.cil.yml</exclude> <!-- flapping timeout -->
@@ -92,6 +93,7 @@ SPDX-License-Identifier: Apache-2.0
     <option name="-skipRecursion"/>
     <!-- SV-Comp files assume that malloc always succeeds -->
     <option name="-setprop">cpa.predicate.memoryAllocationsAlwaysSucceed=true</option>
+    <exclude>../programs/benchmarks/ldv-linux-3.0/module_get_put-drivers-net-sis900.ko.cil.out.yml</exclude> <!-- flapping timeout -->
     <exclude>../programs/benchmarks/ldv-linux-3.4-simple/43_1a_cilled_ok_nondet_linux-43_1a-drivers--i2c--busses--i2c-diolan-u2c.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.yml</exclude> <!-- flapping timeout -->
     <exclude>../programs/benchmarks/ldv-linux-3.4-simple/43_1a_cilled_ok_nondet_linux-43_1a-drivers--media--dvb--frontends--cxd2820r.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.yml</exclude> <!-- flapping timeout -->
     <exclude>../programs/benchmarks/ldv-linux-3.4-simple/43_1a_cilled_ok_nondet_linux-43_1a-drivers--tty--serial--mfd.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.yml</exclude> <!-- flapping timeout -->

test/test-sets/integration-predicate-linear.xml

@@ -50,6 +50,7 @@ SPDX-License-Identifier: Apache-2.0
     <propertyfile>../programs/benchmarks/properties/unreach-call.prp</propertyfile>
     <!-- SV-Comp files assume that malloc always succeeds -->
     <option name="-setprop">cpa.predicate.memoryAllocationsAlwaysSucceed=true</option>
+    <exclude>../programs/benchmarks/loops/vogal-1.yml</exclude> <!-- flapping error (itp failed)/timeout -->
     <exclude>../programs/benchmarks/loop-lit/gj2007.c.i.p+lhb-reducer.yml</exclude> <!-- flapping unknown/timeout -->
     <exclude>../programs/benchmarks/loops-crafted-1/*</exclude> <!-- flapping unknown/timeout -->
     <exclude>../programs/benchmarks/nla-digbench/egcd2-ll.yml</exclude> <!-- flapping unknown/timeout -->
@@ -79,9 +80,11 @@ SPDX-License-Identifier: Apache-2.0
     <option name="-skipRecursion"/>
     <!-- SV-Comp files assume that malloc always succeeds -->
     <option name="-setprop">cpa.predicate.memoryAllocationsAlwaysSucceed=true</option>
+    <exclude>../programs/benchmarks/ldv-linux-3.0/module_get_put-drivers-video-aty-aty128fb.ko.cil.out.yml</exclude> <!-- flapping error/timeout -->
     <exclude>../programs/benchmarks/ldv-linux-3.0/module_get_put-drivers-char-ipmi-ipmi_watchdog.ko.cil.out.yml</exclude> <!-- flapping unknown/timeout -->
     <exclude>../programs/benchmarks/ldv-linux-3.0/module_get_put-drivers-gpu-drm-i915-i915.ko.cil.out.yml</exclude> <!-- flapping unknown/timeout -->
     <exclude>../programs/benchmarks/ldv-linux-3.0/module_get_put-drivers-isdn-mISDN-mISDN_core.ko.cil.out.yml</exclude> <!-- flapping unknown/timeout -->
+    <exclude>../programs/benchmarks/ldv-linux-3.0/module_get_put-drivers-video-aty-aty128fb.ko.cil.out.yml</exclude> <!-- flapping unknown/timeout -->
     <exclude>../programs/benchmarks/ldv-linux-3.4-simple/43_1a_cilled_ok_linux-43_1a-drivers--net--wireless--orinoco--orinoco_usb.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.yml</exclude> <!-- flapping unknown/timeout -->
     <exclude>../programs/benchmarks/ldv-linux-3.4-simple/43_1a_cilled_ok_nondet_linux-43_1a-drivers--media--dvb--frontends--cxd2820r.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.yml</exclude> <!-- flapping unknown/timeout -->
     <exclude>../programs/benchmarks/ldv-linux-3.4-simple/43_1a_cilled_ok_nondet_linux-43_1a-drivers--media--common--tuners--mxl5007t.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.yml</exclude> <!-- flapping unknown/timeout -->

test/test-sets/integration-predicate-overflow.xml

@@ -28,9 +28,12 @@ SPDX-License-Identifier: Apache-2.0
   <tasks name="Overflows-Main">
     <includesfile>../programs/benchmarks/NoOverflows-Main.set</includesfile>
     <propertyfile>../programs/benchmarks/properties/no-overflow.prp</propertyfile>
+    <exclude>../programs/benchmarks/array-lopstr16/partial_lesser_bound.yml</exclude> <!-- flapping timeout / OOM -->
     <exclude>../programs/benchmarks/ldv-commit-tester/m0_sound-oss-opl3-ko--111_1a--42f9f8d-1.yml</exclude> <!-- flapping timeout -->
     <exclude>../programs/benchmarks/ldv-validator-v0.6/linux-stable-42f9f8d-1-111_1a-sound--oss--opl3.ko-entry_point.cil.out.yml</exclude> <!-- flapping unknown/flapping timeout -->
     <exclude>../programs/benchmarks/loop-invgen/nested9.yml</exclude> <!-- flapping timeout -->
+    <exclude>../programs/benchmarks/recursive-simple/fibo_2calls_6-2.yml</exclude> <!-- flapping timeout -->
+    <exclude>../programs/benchmarks/recursive-simple/fibo_7-2.yml</exclude> <!-- flapping timeout -->
   </tasks>
   <tasks name="Overflow-Simple">
     <includesfile>../programs/simple/overflow/overflow.set</includesfile>

test/test-sets/integration-slicingAbstractions-kojak.xml

@@ -74,6 +74,7 @@ SPDX-License-Identifier: Apache-2.0
     <exclude>../programs/benchmarks/ldv-linux-3.4-simple/43_1a_cilled_ok_nondet_linux-43_1a-drivers--media--dvb--dvb-usb--dvb-usb-vp7045.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.yml</exclude> <!-- flapping timeout  -->
     <exclude>../programs/benchmarks/ldv-linux-3.4-simple/43_1a_cilled_ok_nondet_linux-43_1a-drivers--media--dvb--frontends--cxd2820r.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.yml</exclude> <!-- flapping timeout  -->
     <exclude>../programs/benchmarks/ldv-linux-3.4-simple/43_1a_cilled_ok_nondet_linux-43_1a-drivers--mtd--maps--intel_vr_nor.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.yml</exclude> <!-- flapping timeout  -->
+    <exclude>../programs/benchmarks/ldv-linux-3.4-simple/43_1a_cilled_ok_nondet_linux-43_1a-drivers--net--arcnet--com20020_cs.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.yml</exclude> <!-- flapping timeout  -->
     <exclude>../programs/benchmarks/ldv-linux-3.4-simple/43_1a_cilled_ok_nondet_linux-43_1a-drivers--power--wm831x_power.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.yml</exclude> <!-- flapping timeout  -->
     <exclude>../programs/benchmarks/ldv-linux-3.4-simple/43_1a_cilled_ok_nondet_linux-43_1a-drivers--regulator--max8649.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.yml</exclude> <!-- flapping timeout  -->
   </tasks>

test/test-sets/integration-smg.xml

@@ -31,12 +31,14 @@ SPDX-License-Identifier: Apache-2.0
     <includesfile>../programs/benchmarks/MemSafety-Heap.set</includesfile>
     <option name="-smg"/>
     <propertyfile>../programs/benchmarks/properties/valid-memsafety.prp</propertyfile>
+    <exclude>../programs/benchmarks/ldv-memsafety/ArraysOfVariableLength.yml</exclude> <!-- flapping timeout -->
   </tasks>
 
   <tasks name="ArraysMemSafety">
     <includesfile>../programs/benchmarks/MemSafety-Arrays.set</includesfile>
     <option name="-smg"/>
     <propertyfile>../programs/benchmarks/properties/valid-memsafety.prp</propertyfile>
+    <exclude>../programs/benchmarks/termination-memory-alloca/Urban-2013WST-Fig1-alloca.yml</exclude> <!-- flapping timeout -->
   </tasks>
 
   <tasks name="ExtAllocMemSafety">