## SAFARI OPTIONS
#
# . Options may be written in any order
# . Unrecongnized options will throw an error
# . Use '#' for line comments

## SMT-SOLVER:
SMT_solver_path "./z3"
SMT_solver_options "-smt2 -in -nw"


## REFINEMENT OPTIONS
# Refinement strategies:
#  0 -- no refinement (infeasible counterexamples will kill SAFARI)
#  1 -- External Interpolating Prover
#  2 -- Term abstraction
refinement 1`

##  Interpolating theorem prover (the two following options will be ignored if refinement is different from 1)
Interpolating_solver_path "/Users/francesco/usi/opensmt_simone_old1/build/opensmt"
Interpolating_solver_options "--config=opensmt.conf"

## - Execute variabilizer before interpolating prover (enabled if refinement == 1)
## This option allows to execute before executing the interpolating prover
## and after having executed the interpolating prover a script called 'variabilizer.py'
## Such script must be in the same folder of SAFARI.
## SAFARI will execute './variabilizer.py -f ceLog_tmp.smt2 ceLog.smt2' before calling the interpolating prover
## and './variabilizer.py -b interpolants.smt2 SAFARI_interpolants.smt2' when the interpolating prover returns.
variabilizer

## - Pass term abstraction list to the external prover (enabled if refinement == 1)
term_abstraction_list_in_file


## Dotty print
# generates for each refinement the dot of the search space and a log with labels
report

## Minimize the counterexample
ce_minimization



## Auto-certifies the safe inductive invariant
auto_test

## Display the safe inductive invariant
display_safe_invariant