#!/bin/bash
set -Eeuo pipefail
run=$(sed -n -e '/name/{s/.* = *//p}' driver.log)
time=$(sed -n -e '/wall_clock_time/{s/.* = *//p}' driver.log)
value=$(sed -n -e '/* Shortest proof found: /{s///p}' run.log)
code=0
if test -f driver.err; then
  code=$(sed -n -e '/exit_code/{s/.* = *//p}' driver.err)
fi
echo "$run,,$value,$value,$time,$code"
