In termination checking we must not replace loops by assumptions

peterschrammel · peterschrammel · commit 3858c8d791f2 · 2017-11-25T16:48:24.000Z
diff --git a/cbmc.inc b/cbmc.inc
@@ -8,7 +8,7 @@ TOOL_NAME=CBMC
 run()
 {
   if [ "$PROP" = "termination" ] ; then
-    PROPERTY="$PROPERTY --no-assertions"
+    PROPERTY="$PROPERTY --no-assertions --no-self-loops-to-assumptions"
   fi
 
 timeout 875 bash -c ' \

Original file line number	Diff line number	Diff line change
`@@ -8,7 +8,7 @@ TOOL_NAME=CBMC`
`8`	`8`	`run()`
`9`	`9`	`{`
`10`	`10`	`if [ "$PROP" = "termination" ] ; then`
`11`		`- PROPERTY="$PROPERTY --no-assertions"`
	`11`	`+ PROPERTY="$PROPERTY --no-assertions --no-self-loops-to-assumptions"`
`12`	`12`	`fi`
`13`	`13`
`14`	`14`	`timeout 875 bash -c ' \`