Generate not-as-powerful witnesses as the original is faulty

scripts/gen_witness.sh

@@ -4,7 +4,12 @@ BIN=${BASE}/scripts/cpa.sh
 CONF=${BASE}/config/generateWitness.properties
 SPEC=${BASE}/config/specification/sv-comp-reachability.spc
 date1=$(date +"%s")
-${BIN} -heap 10000M -config ${CONF} -spec ${SPEC} -noout $*
+#${BIN} -heap 10000M -config ${CONF} -spec ${SPEC} -noout $*
+if [ -d output ]; then
+  rm -rf output
+fi
+mkdir output
+cp template.graphml output/witness.graphml
 date2=$(date +"%s")
 diff=$(($date2-$date1))
 echo -e "\n*** Witness Generation: $(($diff / 60)) minutes and $(($diff % 60)) seconds elapsed."

template.graphml

@@ -0,0 +1,47 @@
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<graphml xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns="http://graphml.graphdrawing.org/xmlns">
+<key attr.name="assumption" attr.type="string" for="edge" id="assumption"/>
+<key attr.name="sourcecode" attr.type="string" for="edge" id="sourcecode"/>
+<key attr.name="sourcecodeLanguage" attr.type="string" for="graph" id="sourcecodelang"/>
+<key attr.name="control" attr.type="string" for="edge" id="control"/>
+<key attr.name="startline" attr.type="int" for="edge" id="startline"/>
+<key attr.name="originFileName" attr.type="string" for="edge" id="originfile">
+<default>./path.c</default>
+</key>
+<key attr.name="nodeType" attr.type="string" for="node" id="nodetype">
+<default>path</default>
+</key>
+<key attr.name="isFrontierNode" attr.type="boolean" for="node" id="frontier">
+<default>false</default>
+</key>
+<key attr.name="isViolationNode" attr.type="boolean" for="node" id="violation">
+<default>false</default>
+</key>
+<key attr.name="isEntryNode" attr.type="boolean" for="node" id="entry">
+<default>false</default>
+</key>
+<key attr.name="isSinkNode" attr.type="boolean" for="node" id="sink">
+<default>false</default>
+</key>
+<key attr.name="enterFunction" attr.type="string" for="edge" id="enterFunction"/>
+<key attr.name="returnFromFunction" attr.type="string" for="edge" id="returnFrom"/>
+<graph edgedefault="directed"><data key="sourcecodelang">C</data>
+<data key="producer">CPAchecker 1.4-svn 7af0147+</data>
+<data key="programfile">path.c</data>
+<data key="memorymodel">precise</data>
+<data key="architecture">32bit</data>
+<node id="A0">
+<data key="entry">true</data>
+</node>
+<edge source="A0" target="A1"/>
+<node id="A1"/>
+<edge source="A1" target="ERROR"/>
+<node id="ERROR">
+<data key="violation">true</data>
+</node>
+<node id="SINK">
+<data key="sink">true</data>
+</node>
+<edge source="A0" target="SINK"/>
+</graph>
+</graphml>