#!/bin/bash

cvc4=./cvc4
bench="$1"

logic=$(expr "$(grep -m1 '^[^;]*set-logic' "$bench")" : ' *(set-logic  *\([A-Z_]*\) *) *$')

case "$logic" in

QF_BV)
  # run tear-down incremental
  #
  # we run in this way for line-buffered input, otherwise memory's a
  # concern (plus it mimics what we'll end up getting from an
  # application-track trace runner?)
  cat "$bench" | $cvc4 -L smt2 --no-checking --no-interactive --tear-down-incremental
  ;;

*)
  # just run the default --incremental
  #
  # we run in this way for line-buffered input, otherwise memory's a
  # concern (plus it mimics what we'll end up getting from an
  # application-track trace runner?)
  cat "$bench" | $cvc4 -L smt2 --no-checking --no-interactive --incremental
  ;;

esac