diff --git a/cbmc.inc b/cbmc.inc index 5540af9..b77870c 100644 --- a/cbmc.inc +++ b/cbmc.inc @@ -9,6 +9,7 @@ run() { if [ "$PROP" = "termination" ] ; then EC=42 + echo "EC=$EC" >> $LOG.ok return fi @@ -31,7 +32,7 @@ if ! tail -n 10 $LOG.latest | grep -q "^VERIFICATION FAILED$" ; then ec=1 ; fi ; fi ; \ \ case $ec in \ -0) EC=0 ; mv $LOG.latest $LOG.ok ; echo "EC=$EC" >> $LOG.ok ;; \ +0) EC=0 ; mv $LOG.latest $LOG.ok ; echo "EC=$EC" >> $LOG.ok ; break ;; \ 10) EC=10 ; mv $LOG.latest $LOG.ok ; echo "EC=$EC" >> $LOG.ok ; break ;; \ 42) EC=42 ; mv $LOG.latest $LOG.ok ; echo "EC=$EC" >> $LOG.ok ;; \ *) if [ $EC -ne 0 ] ; then EC=$ec ; mv $LOG.latest $LOG.ok ; fi ; echo "EC=$EC" >> $LOG.ok ; break ;; \