contrib/run-script-sygusComp2016-INV

   1 #!/bin/bash
   2
   3 cvc4=./cvc4
   4 bench="$1"
   5
   6 function trywith {
   7   ($cvc4 --lang=sygus --no-checking --no-interactive --dump-synth --default-dag-thresh=0 "$@" $bench) 2>/dev/null |
   8   (read result w1;
   9   case "$result" in
  10   unsat) echo "$w1";cat;exit 0;;
  11   esac; exit 1)
  12   if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
  13 }
  14
  15 trywith --sygus-inv-templ=post
  16