# This is a SARL configuration file.  It specifies information
# about each automated theorem prover available to SARL.

# SARL will look first in the current working directory
# for a file named .sarl.  If it doesn't find that,
# it will look in the same directory for .sarl_default.
# If it doesn't find that, it will look in the user's
# home directory for .sarl, then in the user's home
# directory for sarl_default.

prover {
  alias = cvc4, cvc4x;
  kind = CVC4;
  path = "/opt/local/bin/cvc4";
  options = "--rewrite-divk";
  version = "1.4";
  showQueries = true; # print every query
  timeout = 20.0; # 20 seconds
}

prover {
  alias = cvc3;
  kind = CVC3_API;
  version = "UNKNOWN";
  showQueries = true;
  timeout = 20.0;
}