#!/bin/sh

set -e

export LD_LIBRARY_PATH=$PWD

conv="mono fx7.exe -valid -smt -s -ax:smt/functions.ax"

for d in boogie/{valid,invalid,non-linear} simplify_benchmarks/{front_end_suite,small_suite} ; do
  echo $d/*.smt | xargs rm -f
  no=
  st=unknown
  case $d in
    *front_end* )
      comment="Simplify front end test suite."
      no=-smt-no:1
      st=unsat
    ;;
    boogie/valid* )
    comment="Boogie/Spec# benchmarks."
    st=unsat
    ;;
    boogie/invalid* )
    comment="Boogie/Spec# benchmarks."
    st=sat
    ;;
    *small_su* )
    st=unsat
      comment="Simplify small test suite."
    ;;
  esac
  echo $d/*sx | xargs $conv -o:SmtComment="$comment" $no | tee $(echo $d | sed -e 's@/@-@g').log
  echo $d/*smt | xargs perl -p -i -e 's/:status .*/:status '$st'/'
done