Split witness tests, use inlining for concurrent tests

ultimate-pa · Sep 9, 2024 · 0e8c7e6 · 0e8c7e6
1 parent 0cff8b8
commit 0e8c7e6
Show file tree

Hide file tree

Showing 130 changed files with 308 additions and 220 deletions.
diff --git a/...itness-checking/regression/AutomizerC.epf → ...king/regression/concurrent/AutomizerC.epf b/...itness-checking/regression/AutomizerC.epf → ...king/regression/concurrent/AutomizerC.epf
diff --git a/trunk/examples/witness-checking/regression/concurrent/AutomizerCInline.xml b/trunk/examples/witness-checking/regression/concurrent/AutomizerCInline.xml
@@ -0,0 +1,12 @@
+<rundefinition>
+	<name>Ultimate Toolchain</name>
+	<toolchain>
+
+	<plugin id="de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator"/>
+  <plugin id="de.uni_freiburg.informatik.ultimate.boogie.procedureinliner"/>
+	<plugin id="de.uni_freiburg.informatik.ultimate.boogie.preprocessor"/>
+	<plugin id="de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder"/>
+	<plugin id="de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction"/>
+
+	</toolchain>
+</rundefinition>
diff --git a/...regression/correctness/case_distinction.c → ...concurrent/correctness/case_distinction.c b/...regression/correctness/case_distinction.c → ...concurrent/correctness/case_distinction.c
diff --git a/...orrectness/case_distinction.c-witness.yml → ...orrectness/case_distinction.c-witness.yml b/...orrectness/case_distinction.c-witness.yml → ...orrectness/case_distinction.c-witness.yml
diff --git a/...s-checking/regression/correctness/mutex.c → ...regression/concurrent/correctness/mutex.c b/...s-checking/regression/correctness/mutex.c → ...regression/concurrent/correctness/mutex.c
diff --git a/...egression/correctness/mutex.c-witness.yml → ...oncurrent/correctness/mutex.c-witness.yml b/...egression/correctness/mutex.c-witness.yml → ...oncurrent/correctness/mutex.c-witness.yml
diff --git a/...cking/regression/correctness/nondet_inc.c → ...ssion/concurrent/correctness/nondet_inc.c b/...cking/regression/correctness/nondet_inc.c → ...ssion/concurrent/correctness/nondet_inc.c
diff --git a/...sion/correctness/nondet_inc.c-witness.yml → ...rent/correctness/nondet_inc.c-witness.yml b/...sion/correctness/nondet_inc.c-witness.yml → ...rent/correctness/nondet_inc.c-witness.yml
diff --git a/trunk/examples/witness-checking/regression/sequential/AutomizerC.epf b/trunk/examples/witness-checking/regression/sequential/AutomizerC.epf
@@ -0,0 +1,76 @@
+#Mon Nov 27 17:23:30 CET 2017
+\!/instance/de.uni_freiburg.informatik.ultimate.core=
+/instance/de.uni_freiburg.informatik.ultimate.core/Log\ level\ for\ class=de.uni_freiburg.informatik.ultimate.lib.smtlibutils.quantifier.QuantifierPusher\=ERROR;
+file_export_version=3.0
+@de.uni_freiburg.informatik.ultimate.core=0.1.22
+
+
+#Fri Oct 24 16:34:36 CEST 2014
+\!/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator=
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator/sizeof\ long=4
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator/sizeof\ POINTER=4
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator/sizeof\ long\ double=12
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator/Check\ division\ by\ zero=IGNORE
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator/Check\ if\ freed\ pointer\ was\ valid=false
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator/Pointer\ to\ allocated\ memory\ at\ dereference=IGNORE
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator/Check\ array\ bounds\ for\ arrays\ that\ are\ off\ heap=IGNORE
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator/Check\ for\ the\ main\ procedure\ if\ all\ allocated\ memory\ was\ freed=false
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator/If\ two\ pointers\ are\ subtracted\ or\ compared\ they\ have\ the\ same\ base\ address=IGNORE
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator/Pointer\ base\ address\ is\ valid\ at\ dereference=IGNORE
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator/Overapproximate\ operations\ on\ floating\ types=true
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator/Use\ constant\ arrays=true
+@de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator=0.0.1
+
+
+#Fri Oct 24 16:34:36 CEST 2014
+\!/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder=
+file_export_version=3.0
+@de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder=0.0.1
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder/Convert\ code\ blocks\ to\ CNF=false
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder/Size\ of\ a\ code\ block=SequenceOfStatements
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder/Command\ for\ external\ solver=z3 SMTLIB2_COMPLIANT\=true -memory\:2024 -smt2 -in -t\:2000
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder/SMT\ solver=External_DefaultMode
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder/Dump\ SMT\ script\ to\ file=false
+
+
+#Thu Nov 06 16:26:23 CET 2014
+\!/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction=
+file_export_version=3.0
+@de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction=0.0.1
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Interpolants\ consolidation=false
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Compute\ Interpolants\ along\ a\ Counterexample=FPandBP
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Use\ separate\ solver\ for\ trace\ checks=true
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/SMT\ solver=External_ModelsAndUnsatCoreMode
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Command\ for\ external\ solver=z3 SMTLIB2_COMPLIANT\=true -memory\:2024 -smt2 -in
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Positions\ where\ we\ compute\ the\ Hoare\ Annotation=LoopHeads
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Trace\ refinement\ strategy=CAMEL
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Trace\ refinement\ exception\ blacklist=DEPENDING
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Automaton\ type\ used\ in\ concurrency\ analysis=PETRI_NET
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Apply\ one-shot\ large\ block\ encoding\ in\ concurrent\ analysis=true
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Independence\ relation\ used\ for\ large\ block\ encoding\ in\ concurrent\ analysis=SYNTACTIC
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Looper\ check\ in\ Petri\ net\ analysis=SEMANTIC
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Order\ on\ configurations\ for\ Petri\ net\ unfoldings=DBO
+
+
+#Thu Oct 29 23:01:13 CET 2015
+file_export_version=3.0
+@de.uni_freiburg.informatik.ultimate.boogie.procedureinliner=0.0.1
+\!/instance/de.uni_freiburg.informatik.ultimate.boogie.procedureinliner=
+/instance/de.uni_freiburg.informatik.ultimate.boogie.procedureinliner/Ignore\ calls\ to\ procedures\ called\ more\ than\ once=ONLY_FOR_SEQUENTIAL_PROGRAMS
+
+
+#Tue Nov 21 08:04:41 CET 2017
+\!/instance/de.uni_freiburg.informatik.ultimate.plugins.blockencoding=
+file_export_version=3.0
+@de.uni_freiburg.informatik.ultimate.plugins.blockencoding=0.1.22
+/instance/de.uni_freiburg.informatik.ultimate.plugins.blockencoding/Simplify\ transitions=false
+/instance/de.uni_freiburg.informatik.ultimate.plugins.blockencoding/Apply\ optimizations\ until\ nothing\ changes=true
+/instance/de.uni_freiburg.informatik.ultimate.plugins.blockencoding/Create\ parallel\ compositions\ if\ possible=false
+/instance/de.uni_freiburg.informatik.ultimate.plugins.blockencoding/Remove\ sink\ states=true
+/instance/de.uni_freiburg.informatik.ultimate.plugins.blockencoding/Rewrite\ not-equals=false
+/instance/de.uni_freiburg.informatik.ultimate.plugins.blockencoding/Iterate\ optimizations\ for\ n\ times\ (<\=0\ means\ until\ nothing\ changes)=0
+/instance/de.uni_freiburg.informatik.ultimate.plugins.blockencoding/Create\ interprocedural\ compositions=true
+/instance/de.uni_freiburg.informatik.ultimate.plugins.blockencoding/Remove\ infeasible\ edges=true
+/instance/de.uni_freiburg.informatik.ultimate.plugins.blockencoding/Maximize\ final\ states=true
+/instance/de.uni_freiburg.informatik.ultimate.plugins.blockencoding/Use\ SBE=true
+/instance/de.uni_freiburg.informatik.ultimate.plugins.blockencoding/Minimize\ states\ even\ if\ more\ edges\ are\ added\ than\ removed.=false
diff --git a/...itness-checking/regression/AutomizerC.xml → ...king/regression/sequential/AutomizerC.xml b/...itness-checking/regression/AutomizerC.xml → ...king/regression/sequential/AutomizerC.xml
diff --git a/...egression/correctness/SpamAssassin-loop.i → ...equential/correctness/SpamAssassin-loop.i b/...egression/correctness/SpamAssassin-loop.i → ...equential/correctness/SpamAssassin-loop.i
diff --git a/...tness/SpamAssassin-loop.i-witness.graphml → ...tness/SpamAssassin-loop.i-witness.graphml b/...tness/SpamAssassin-loop.i-witness.graphml → ...tness/SpamAssassin-loop.i-witness.graphml
diff --git a/...ess/SpamAssassin-loop.i-witness_v0.1.yaml → ...ess/SpamAssassin-loop.i-witness_v0.1.yaml b/...ess/SpamAssassin-loop.i-witness_v0.1.yaml → ...ess/SpamAssassin-loop.i-witness_v0.1.yaml
diff --git a/...ctness/SpamAssassin-loop.i-witness_v2.yml → ...ctness/SpamAssassin-loop.i-witness_v2.yml b/...ctness/SpamAssassin-loop.i-witness_v2.yml → ...ctness/SpamAssassin-loop.i-witness_v2.yml
diff --git a/...g/regression/correctness/apache-get-tag.i → ...n/sequential/correctness/apache-get-tag.i b/...g/regression/correctness/apache-get-tag.i → ...n/sequential/correctness/apache-get-tag.i
diff --git a/...rectness/apache-get-tag.i-witness.graphml → ...rectness/apache-get-tag.i-witness.graphml b/...rectness/apache-get-tag.i-witness.graphml → ...rectness/apache-get-tag.i-witness.graphml
diff --git a/...ctness/apache-get-tag.i-witness_v0.1.yaml → ...ctness/apache-get-tag.i-witness_v0.1.yaml b/...ctness/apache-get-tag.i-witness_v0.1.yaml → ...ctness/apache-get-tag.i-witness_v0.1.yaml
diff --git a/...rrectness/apache-get-tag.i-witness_v2.yml → ...rrectness/apache-get-tag.i-witness_v2.yml b/...rrectness/apache-get-tag.i-witness_v2.yml → ...rrectness/apache-get-tag.i-witness_v2.yml
diff --git a/...gression/correctness/benchmark26_linear.i → ...quential/correctness/benchmark26_linear.i b/...gression/correctness/benchmark26_linear.i → ...quential/correctness/benchmark26_linear.i
diff --git a/...ness/benchmark26_linear.i-witness.graphml → ...ness/benchmark26_linear.i-witness.graphml b/...ness/benchmark26_linear.i-witness.graphml → ...ness/benchmark26_linear.i-witness.graphml
diff --git a/...ss/benchmark26_linear.i-witness_v0.1.yaml → ...ss/benchmark26_linear.i-witness_v0.1.yaml b/...ss/benchmark26_linear.i-witness_v0.1.yaml → ...ss/benchmark26_linear.i-witness_v0.1.yaml
diff --git a/...tness/benchmark26_linear.i-witness_v2.yml → ...tness/benchmark26_linear.i-witness_v2.yml b/...tness/benchmark26_linear.i-witness_v2.yml → ...tness/benchmark26_linear.i-witness_v2.yml
diff --git a/...gression/correctness/benchmark35_linear.i → ...quential/correctness/benchmark35_linear.i b/...gression/correctness/benchmark35_linear.i → ...quential/correctness/benchmark35_linear.i
diff --git a/...ness/benchmark35_linear.i-witness.graphml → ...ness/benchmark35_linear.i-witness.graphml b/...ness/benchmark35_linear.i-witness.graphml → ...ness/benchmark35_linear.i-witness.graphml
diff --git a/...ss/benchmark35_linear.i-witness_v0.1.yaml → ...ss/benchmark35_linear.i-witness_v0.1.yaml b/...ss/benchmark35_linear.i-witness_v0.1.yaml → ...ss/benchmark35_linear.i-witness_v0.1.yaml
diff --git a/...tness/benchmark35_linear.i-witness_v2.yml → ...tness/benchmark35_linear.i-witness_v2.yml b/...tness/benchmark35_linear.i-witness_v2.yml → ...tness/benchmark35_linear.i-witness_v2.yml
diff --git a/...checking/regression/correctness/bitwise.c → ...gression/sequential/correctness/bitwise.c b/...checking/regression/correctness/bitwise.c → ...gression/sequential/correctness/bitwise.c
diff --git a/...ression/correctness/bitwise.c-witness.yml → ...uential/correctness/bitwise.c-witness.yml b/...ression/correctness/bitwise.c-witness.yml → ...uential/correctness/bitwise.c-witness.yml
diff --git a/...king/regression/correctness/cohendiv-ll.c → ...sion/sequential/correctness/cohendiv-ll.c b/...king/regression/correctness/cohendiv-ll.c → ...sion/sequential/correctness/cohendiv-ll.c
diff --git a/...correctness/cohendiv-ll.c-witness.graphml → ...correctness/cohendiv-ll.c-witness.graphml b/...correctness/cohendiv-ll.c-witness.graphml → ...correctness/cohendiv-ll.c-witness.graphml
diff --git a/...rrectness/cohendiv-ll.c-witness_v0.1.yaml → ...rrectness/cohendiv-ll.c-witness_v0.1.yaml b/...rrectness/cohendiv-ll.c-witness_v0.1.yaml → ...rrectness/cohendiv-ll.c-witness_v0.1.yaml
diff --git a/.../correctness/cohendiv-ll.c-witness_v2.yml → .../correctness/cohendiv-ll.c-witness_v2.yml b/.../correctness/cohendiv-ll.c-witness_v2.yml → .../correctness/cohendiv-ll.c-witness_v2.yml
diff --git a/...s-checking/regression/correctness/const.c → ...regression/sequential/correctness/const.c b/...s-checking/regression/correctness/const.c → ...regression/sequential/correctness/const.c
diff --git a/...ssion/correctness/const.c-witness.graphml → ...ntial/correctness/const.c-witness.graphml b/...ssion/correctness/const.c-witness.graphml → ...ntial/correctness/const.c-witness.graphml
diff --git a/...ion/correctness/const.c-witness_v0.1.yaml → ...ial/correctness/const.c-witness_v0.1.yaml b/...ion/correctness/const.c-witness_v0.1.yaml → ...ial/correctness/const.c-witness_v0.1.yaml
diff --git a/...ession/correctness/const.c-witness_v2.yml → ...ential/correctness/const.c-witness_v2.yml b/...ession/correctness/const.c-witness_v2.yml → ...ential/correctness/const.c-witness_v2.yml
diff --git a/...hecking/regression/correctness/contract.c → ...ression/sequential/correctness/contract.c b/...hecking/regression/correctness/contract.c → ...ression/sequential/correctness/contract.c
diff --git a/...ession/correctness/contract.c-witness.yml → ...ential/correctness/contract.c-witness.yml b/...ession/correctness/contract.c-witness.yml → ...ential/correctness/contract.c-witness.yml
diff --git a/...ecking/regression/correctness/contract2.c → ...ession/sequential/correctness/contract2.c b/...ecking/regression/correctness/contract2.c → ...ession/sequential/correctness/contract2.c
diff --git a/...ssion/correctness/contract2.c-witness.yml → ...ntial/correctness/contract2.c-witness.yml b/...ssion/correctness/contract2.c-witness.yml → ...ntial/correctness/contract2.c-witness.yml
diff --git a/...cking/regression/correctness/doubleLoop.c → ...ssion/sequential/correctness/doubleLoop.c b/...cking/regression/correctness/doubleLoop.c → ...ssion/sequential/correctness/doubleLoop.c
diff --git a/.../correctness/doubleLoop.c-witness.graphml → .../correctness/doubleLoop.c-witness.graphml b/.../correctness/doubleLoop.c-witness.graphml → .../correctness/doubleLoop.c-witness.graphml
diff --git a/...orrectness/doubleLoop.c-witness_v0.1.yaml → ...orrectness/doubleLoop.c-witness_v0.1.yaml b/...orrectness/doubleLoop.c-witness_v0.1.yaml → ...orrectness/doubleLoop.c-witness_v0.1.yaml
diff --git a/...n/correctness/doubleLoop.c-witness_v2.yml → ...l/correctness/doubleLoop.c-witness_v2.yml b/...n/correctness/doubleLoop.c-witness_v2.yml → ...l/correctness/doubleLoop.c-witness_v2.yml
diff --git a/...hecking/regression/correctness/for_loop.c → ...ression/sequential/correctness/for_loop.c b/...hecking/regression/correctness/for_loop.c → ...ression/sequential/correctness/for_loop.c
diff --git a/...on/correctness/for_loop.c-witness.graphml → ...al/correctness/for_loop.c-witness.graphml b/...on/correctness/for_loop.c-witness.graphml → ...al/correctness/for_loop.c-witness.graphml
diff --git a/.../correctness/for_loop.c-witness_v0.1.yaml → .../correctness/for_loop.c-witness_v0.1.yaml b/.../correctness/for_loop.c-witness_v0.1.yaml → .../correctness/for_loop.c-witness_v0.1.yaml
diff --git a/...ion/correctness/for_loop.c-witness_v2.yml → ...ial/correctness/for_loop.c-witness_v2.yml b/...ion/correctness/for_loop.c-witness_v2.yml → ...ial/correctness/for_loop.c-witness_v2.yml
diff --git a/...checking/regression/correctness/gsv2008.i → ...gression/sequential/correctness/gsv2008.i b/...checking/regression/correctness/gsv2008.i → ...gression/sequential/correctness/gsv2008.i
diff --git a/...ion/correctness/gsv2008.i-witness.graphml → ...ial/correctness/gsv2008.i-witness.graphml b/...ion/correctness/gsv2008.i-witness.graphml → ...ial/correctness/gsv2008.i-witness.graphml
diff --git a/...n/correctness/gsv2008.i-witness_v0.1.yaml → ...l/correctness/gsv2008.i-witness_v0.1.yaml b/...n/correctness/gsv2008.i-witness_v0.1.yaml → ...l/correctness/gsv2008.i-witness_v0.1.yaml
diff --git a/...sion/correctness/gsv2008.i-witness_v2.yml → ...tial/correctness/gsv2008.i-witness_v2.yml b/...sion/correctness/gsv2008.i-witness_v2.yml → ...tial/correctness/gsv2008.i-witness_v2.yml
diff --git a/...orrectness/implicitunsignedconversion-2.c → ...orrectness/implicitunsignedconversion-2.c b/...orrectness/implicitunsignedconversion-2.c → ...orrectness/implicitunsignedconversion-2.c
diff --git a/...citunsignedconversion-2.c-witness.graphml → ...citunsignedconversion-2.c-witness.graphml b/...citunsignedconversion-2.c-witness.graphml → ...citunsignedconversion-2.c-witness.graphml
diff --git a/...tunsignedconversion-2.c-witness_v0.1.yaml → ...tunsignedconversion-2.c-witness_v0.1.yaml b/...tunsignedconversion-2.c-witness_v0.1.yaml → ...tunsignedconversion-2.c-witness_v0.1.yaml
diff --git a/...icitunsignedconversion-2.c-witness_v2.yml → ...icitunsignedconversion-2.c-witness_v2.yml b/...icitunsignedconversion-2.c-witness_v2.yml → ...icitunsignedconversion-2.c-witness_v2.yml
diff --git a/...hecking/regression/correctness/jain_6-1.c → ...ression/sequential/correctness/jain_6-1.c b/...hecking/regression/correctness/jain_6-1.c → ...ression/sequential/correctness/jain_6-1.c
diff --git a/...on/correctness/jain_6-1.c-witness.graphml → ...al/correctness/jain_6-1.c-witness.graphml b/...on/correctness/jain_6-1.c-witness.graphml → ...al/correctness/jain_6-1.c-witness.graphml
diff --git a/.../correctness/jain_6-1.c-witness_v0.1.yaml → .../correctness/jain_6-1.c-witness_v0.1.yaml b/.../correctness/jain_6-1.c-witness_v0.1.yaml → .../correctness/jain_6-1.c-witness_v0.1.yaml
diff --git a/...ion/correctness/jain_6-1.c-witness_v2.yml → ...ial/correctness/jain_6-1.c-witness_v2.yml b/...ion/correctness/jain_6-1.c-witness_v2.yml → ...ial/correctness/jain_6-1.c-witness_v2.yml
diff --git a/...sion/correctness/loop_as_goto-witness.yml → ...tial/correctness/loop_as_goto-witness.yml b/...sion/correctness/loop_as_goto-witness.yml → ...tial/correctness/loop_as_goto-witness.yml
diff --git a/...ing/regression/correctness/loop_as_goto.c → ...ion/sequential/correctness/loop_as_goto.c b/...ing/regression/correctness/loop_as_goto.c → ...ion/sequential/correctness/loop_as_goto.c
diff --git a/...hecking/regression/correctness/mannadiv.c → ...ression/sequential/correctness/mannadiv.c b/...hecking/regression/correctness/mannadiv.c → ...ression/sequential/correctness/mannadiv.c
diff --git a/...on/correctness/mannadiv.c-witness.graphml → ...al/correctness/mannadiv.c-witness.graphml b/...on/correctness/mannadiv.c-witness.graphml → ...al/correctness/mannadiv.c-witness.graphml
diff --git a/.../correctness/mannadiv.c-witness_v0.1.yaml → .../correctness/mannadiv.c-witness_v0.1.yaml b/.../correctness/mannadiv.c-witness_v0.1.yaml → .../correctness/mannadiv.c-witness_v0.1.yaml
diff --git a/...ion/correctness/mannadiv.c-witness_v2.yml → ...ial/correctness/mannadiv.c-witness_v2.yml b/...ion/correctness/mannadiv.c-witness_v2.yml → ...ial/correctness/mannadiv.c-witness_v2.yml
diff --git a/...ss-checking/regression/correctness/mod3.c → .../regression/sequential/correctness/mod3.c b/...ss-checking/regression/correctness/mod3.c → .../regression/sequential/correctness/mod3.c
diff --git a/...ession/correctness/mod3.c-witness.graphml → ...ential/correctness/mod3.c-witness.graphml b/...ession/correctness/mod3.c-witness.graphml → ...ential/correctness/mod3.c-witness.graphml
diff --git a/...egression/correctness/mod3.c-witness.yaml → ...equential/correctness/mod3.c-witness.yaml b/...egression/correctness/mod3.c-witness.yaml → ...equential/correctness/mod3.c-witness.yaml
diff --git a/...s-checking/regression/correctness/n.c11.c → ...regression/sequential/correctness/n.c11.c b/...s-checking/regression/correctness/n.c11.c → ...regression/sequential/correctness/n.c11.c
diff --git a/...ssion/correctness/n.c11.c-witness.graphml → ...ntial/correctness/n.c11.c-witness.graphml b/...ssion/correctness/n.c11.c-witness.graphml → ...ntial/correctness/n.c11.c-witness.graphml
diff --git a/...ion/correctness/n.c11.c-witness_v0.1.yaml → ...ial/correctness/n.c11.c-witness_v0.1.yaml b/...ion/correctness/n.c11.c-witness_v0.1.yaml → ...ial/correctness/n.c11.c-witness_v0.1.yaml
diff --git a/...ession/correctness/n.c11.c-witness_v2.yml → ...ential/correctness/n.c11.c-witness_v2.yml b/...ession/correctness/n.c11.c-witness_v2.yml → ...ential/correctness/n.c11.c-witness_v2.yml
diff --git a/...ess-checking/regression/correctness/odd.c → ...g/regression/sequential/correctness/odd.c b/...ess-checking/regression/correctness/odd.c → ...g/regression/sequential/correctness/odd.c
diff --git a/...ression/correctness/odd.c-witness.graphml → ...uential/correctness/odd.c-witness.graphml b/...ression/correctness/odd.c-witness.graphml → ...uential/correctness/odd.c-witness.graphml
diff --git a/...regression/correctness/odd.c-witness.yaml → ...sequential/correctness/odd.c-witness.yaml b/...regression/correctness/odd.c-witness.yaml → ...sequential/correctness/odd.c-witness.yaml
diff --git a/...ing/regression/correctness/overflow_1-1.c → ...ion/sequential/correctness/overflow_1-1.c b/...ing/regression/correctness/overflow_1-1.c → ...ion/sequential/correctness/overflow_1-1.c
diff --git a/...orrectness/overflow_1-1.c-witness.graphml → ...orrectness/overflow_1-1.c-witness.graphml b/...orrectness/overflow_1-1.c-witness.graphml → ...orrectness/overflow_1-1.c-witness.graphml
diff --git a/...rectness/overflow_1-1.c-witness_v0.1.yaml → ...rectness/overflow_1-1.c-witness_v0.1.yaml b/...rectness/overflow_1-1.c-witness_v0.1.yaml → ...rectness/overflow_1-1.c-witness_v0.1.yaml
diff --git a/...correctness/overflow_1-1.c-witness_v2.yml → ...correctness/overflow_1-1.c-witness_v2.yml b/...correctness/overflow_1-1.c-witness_v2.yml → ...correctness/overflow_1-1.c-witness_v2.yml
diff --git a/...checking/regression/correctness/pointer.c → ...gression/sequential/correctness/pointer.c b/...checking/regression/correctness/pointer.c → ...gression/sequential/correctness/pointer.c
diff --git a/...ession/correctness/pointer.c-witness.yaml → ...ential/correctness/pointer.c-witness.yaml b/...ession/correctness/pointer.c-witness.yaml → ...ential/correctness/pointer.c-witness.yaml
diff --git a/...cking/regression/correctness/psyco_io_1.c → ...ssion/sequential/correctness/psyco_io_1.c b/...cking/regression/correctness/psyco_io_1.c → ...ssion/sequential/correctness/psyco_io_1.c
diff --git a/.../correctness/psyco_io_1.c-witness.graphml → .../correctness/psyco_io_1.c-witness.graphml b/.../correctness/psyco_io_1.c-witness.graphml → .../correctness/psyco_io_1.c-witness.graphml
diff --git a/...orrectness/psyco_io_1.c-witness_v0.1.yaml → ...orrectness/psyco_io_1.c-witness_v0.1.yaml b/...orrectness/psyco_io_1.c-witness_v0.1.yaml → ...orrectness/psyco_io_1.c-witness_v0.1.yaml
diff --git a/...n/correctness/psyco_io_1.c-witness_v2.yml → ...l/correctness/psyco_io_1.c-witness_v2.yml b/...n/correctness/psyco_io_1.c-witness_v2.yml → ...l/correctness/psyco_io_1.c-witness_v2.yml
diff --git a/...g/regression/correctness/psyco_security.c → ...n/sequential/correctness/psyco_security.c b/...g/regression/correctness/psyco_security.c → ...n/sequential/correctness/psyco_security.c
diff --git a/...rectness/psyco_security.c-witness.graphml → ...rectness/psyco_security.c-witness.graphml b/...rectness/psyco_security.c-witness.graphml → ...rectness/psyco_security.c-witness.graphml
diff --git a/...ctness/psyco_security.c-witness_v0.1.yaml → ...ctness/psyco_security.c-witness_v0.1.yaml b/...ctness/psyco_security.c-witness_v0.1.yaml → ...ctness/psyco_security.c-witness_v0.1.yaml
diff --git a/...rrectness/psyco_security.c-witness_v2.yml → ...rrectness/psyco_security.c-witness_v2.yml b/...rrectness/psyco_security.c-witness_v2.yml → ...rrectness/psyco_security.c-witness_v2.yml
diff --git a/...regression/correctness/quick_sort_split.i → ...sequential/correctness/quick_sort_split.i b/...regression/correctness/quick_sort_split.i → ...sequential/correctness/quick_sort_split.i
diff --git a/...ctness/quick_sort_split.i-witness.graphml → ...ctness/quick_sort_split.i-witness.graphml b/...ctness/quick_sort_split.i-witness.graphml → ...ctness/quick_sort_split.i-witness.graphml
diff --git a/...ness/quick_sort_split.i-witness_v0.1.yaml → ...ness/quick_sort_split.i-witness_v0.1.yaml b/...ness/quick_sort_split.i-witness_v0.1.yaml → ...ness/quick_sort_split.i-witness_v0.1.yaml
diff --git a/...ectness/quick_sort_split.i-witness_v2.yml → ...ectness/quick_sort_split.i-witness_v2.yml b/...ectness/quick_sort_split.i-witness_v2.yml → ...ectness/quick_sort_split.i-witness_v2.yml
diff --git a/...regression/correctness/signextension2-1.c → ...sequential/correctness/signextension2-1.c b/...regression/correctness/signextension2-1.c → ...sequential/correctness/signextension2-1.c
diff --git a/...ctness/signextension2-1.c-witness.graphml → ...ctness/signextension2-1.c-witness.graphml b/...ctness/signextension2-1.c-witness.graphml → ...ctness/signextension2-1.c-witness.graphml
diff --git a/...ness/signextension2-1.c-witness_v0.1.yaml → ...ness/signextension2-1.c-witness_v0.1.yaml b/...ness/signextension2-1.c-witness_v0.1.yaml → ...ness/signextension2-1.c-witness_v0.1.yaml
diff --git a/...ectness/signextension2-1.c-witness_v2.yml → ...ectness/signextension2-1.c-witness_v2.yml b/...ectness/signextension2-1.c-witness_v2.yml → ...ectness/signextension2-1.c-witness_v2.yml
diff --git a/.../regression/correctness/simple_vardep_1.c → .../sequential/correctness/simple_vardep_1.c b/.../regression/correctness/simple_vardep_1.c → .../sequential/correctness/simple_vardep_1.c
diff --git a/...ectness/simple_vardep_1.c-witness.graphml → ...ectness/simple_vardep_1.c-witness.graphml b/...ectness/simple_vardep_1.c-witness.graphml → ...ectness/simple_vardep_1.c-witness.graphml
diff --git a/...tness/simple_vardep_1.c-witness_v0.1.yaml → ...tness/simple_vardep_1.c-witness_v0.1.yaml b/...tness/simple_vardep_1.c-witness_v0.1.yaml → ...tness/simple_vardep_1.c-witness_v0.1.yaml
diff --git a/...rectness/simple_vardep_1.c-witness_v2.yml → ...rectness/simple_vardep_1.c-witness_v2.yml b/...rectness/simple_vardep_1.c-witness_v2.yml → ...rectness/simple_vardep_1.c-witness_v2.yml
diff --git a/.../regression/correctness/simple_vardep_2.c → .../sequential/correctness/simple_vardep_2.c b/.../regression/correctness/simple_vardep_2.c → .../sequential/correctness/simple_vardep_2.c
diff --git a/...ectness/simple_vardep_2.c-witness.graphml → ...ectness/simple_vardep_2.c-witness.graphml b/...ectness/simple_vardep_2.c-witness.graphml → ...ectness/simple_vardep_2.c-witness.graphml
diff --git a/...orrectness/simple_vardep_2.c-witness.yaml → ...orrectness/simple_vardep_2.c-witness.yaml b/...orrectness/simple_vardep_2.c-witness.yaml → ...orrectness/simple_vardep_2.c-witness.yaml
diff --git a/...rectness/simple_vardep_2.c-witness_v2.yml → ...rectness/simple_vardep_2.c-witness_v2.yml b/...rectness/simple_vardep_2.c-witness_v2.yml → ...rectness/simple_vardep_2.c-witness_v2.yml
diff --git a/...cking/regression/correctness/singleLine.c → ...ssion/sequential/correctness/singleLine.c b/...cking/regression/correctness/singleLine.c → ...ssion/sequential/correctness/singleLine.c
diff --git a/...sion/correctness/singleLine.c-witness.yml → ...tial/correctness/singleLine.c-witness.yml b/...sion/correctness/singleLine.c-witness.yml → ...tial/correctness/singleLine.c-witness.yml
diff --git a/...ssion/correctness/sqrt1-ll_valuebound20.c → ...ntial/correctness/sqrt1-ll_valuebound20.c b/...ssion/correctness/sqrt1-ll_valuebound20.c → ...ntial/correctness/sqrt1-ll_valuebound20.c
diff --git a/...s/sqrt1-ll_valuebound20.c-witness.graphml → ...s/sqrt1-ll_valuebound20.c-witness.graphml b/...s/sqrt1-ll_valuebound20.c-witness.graphml → ...s/sqrt1-ll_valuebound20.c-witness.graphml
diff --git a/...sqrt1-ll_valuebound20.c-witness_v0.1.yaml → ...sqrt1-ll_valuebound20.c-witness_v0.1.yaml b/...sqrt1-ll_valuebound20.c-witness_v0.1.yaml → ...sqrt1-ll_valuebound20.c-witness_v0.1.yaml
diff --git a/...ss/sqrt1-ll_valuebound20.c-witness_v2.yml → ...ss/sqrt1-ll_valuebound20.c-witness_v2.yml b/...ss/sqrt1-ll_valuebound20.c-witness_v2.yml → ...ss/sqrt1-ll_valuebound20.c-witness_v2.yml
diff --git a/...s-checking/regression/correctness/sumt5.c → ...regression/sequential/correctness/sumt5.c b/...s-checking/regression/correctness/sumt5.c → ...regression/sequential/correctness/sumt5.c
diff --git a/...ssion/correctness/sumt5.c-witness.graphml → ...ntial/correctness/sumt5.c-witness.graphml b/...ssion/correctness/sumt5.c-witness.graphml → ...ntial/correctness/sumt5.c-witness.graphml
diff --git a/...ion/correctness/sumt5.c-witness_v0.1.yaml → ...ial/correctness/sumt5.c-witness_v0.1.yaml b/...ion/correctness/sumt5.c-witness_v0.1.yaml → ...ial/correctness/sumt5.c-witness_v0.1.yaml
diff --git a/...ession/correctness/sumt5.c-witness_v2.yml → ...ential/correctness/sumt5.c-witness_v2.yml b/...ession/correctness/sumt5.c-witness_v2.yml → ...ential/correctness/sumt5.c-witness_v2.yml
diff --git a/...s-checking/regression/correctness/sumt9.c → ...regression/sequential/correctness/sumt9.c b/...s-checking/regression/correctness/sumt9.c → ...regression/sequential/correctness/sumt9.c
diff --git a/...ssion/correctness/sumt9.c-witness.graphml → ...ntial/correctness/sumt9.c-witness.graphml b/...ssion/correctness/sumt9.c-witness.graphml → ...ntial/correctness/sumt9.c-witness.graphml
diff --git a/...ion/correctness/sumt9.c-witness_v0.1.yaml → ...ial/correctness/sumt9.c-witness_v0.1.yaml b/...ion/correctness/sumt9.c-witness_v0.1.yaml → ...ial/correctness/sumt9.c-witness_v0.1.yaml
diff --git a/...ession/correctness/sumt9.c-witness_v2.yml → ...ential/correctness/sumt9.c-witness_v2.yml b/...ession/correctness/sumt9.c-witness_v2.yml → ...ential/correctness/sumt9.c-witness_v2.yml
diff --git a/...ing/regression/correctness/test_locks_5.c → ...ion/sequential/correctness/test_locks_5.c b/...ing/regression/correctness/test_locks_5.c → ...ion/sequential/correctness/test_locks_5.c
diff --git a/...orrectness/test_locks_5.c-witness.graphml → ...orrectness/test_locks_5.c-witness.graphml b/...orrectness/test_locks_5.c-witness.graphml → ...orrectness/test_locks_5.c-witness.graphml
diff --git a/...rectness/test_locks_5.c-witness_v0.1.yaml → ...rectness/test_locks_5.c-witness_v0.1.yaml b/...rectness/test_locks_5.c-witness_v0.1.yaml → ...rectness/test_locks_5.c-witness_v0.1.yaml
diff --git a/...correctness/test_locks_5.c-witness_v2.yml → ...correctness/test_locks_5.c-witness_v2.yml b/...correctness/test_locks_5.c-witness_v2.yml → ...correctness/test_locks_5.c-witness_v2.yml
diff --git a/...hecking/regression/correctness/trex01-2.i → ...ression/sequential/correctness/trex01-2.i b/...hecking/regression/correctness/trex01-2.i → ...ression/sequential/correctness/trex01-2.i
diff --git a/...on/correctness/trex01-2.i-witness.graphml → ...al/correctness/trex01-2.i-witness.graphml b/...on/correctness/trex01-2.i-witness.graphml → ...al/correctness/trex01-2.i-witness.graphml
diff --git a/.../correctness/trex01-2.i-witness_v0.1.yaml → .../correctness/trex01-2.i-witness_v0.1.yaml b/.../correctness/trex01-2.i-witness_v0.1.yaml → .../correctness/trex01-2.i-witness_v0.1.yaml
diff --git a/...ion/correctness/trex01-2.i-witness_v2.yml → ...ial/correctness/trex01-2.i-witness_v2.yml b/...ion/correctness/trex01-2.i-witness_v2.yml → ...ial/correctness/trex01-2.i-witness_v2.yml