CSIsat is an open-source interpolating decision procedure for LA+EUF.

Usage:
Reads the query from stdin and writes the result to stdout.

If the input formula is satisfiable, 
CSIsat writes "Satisfiable: <formula>" on stderr.
'formula' implies the conjunction of the two input formula.
Otherwise it writes an interpolant to stdout.
The computed interpolant can be verified with option -check.

Options:
--------
-debug   Print debug information.
-check   Check the computed interpolant (consumes additional runtime).
-sat     Check for satisfiability only (no interpolation).
         Writes only "satisfiable" or "unsatisfiable" to stdout.
-LAsolver Choose the LA solver to use.
         Options: simplex, simplex_wo_presolve, interior, exact (default: simplex).
         WARNING: exact solver integration is still experimental.
-SATsolver Choose the SAT solver to use.
         Options: csi_dpll, pico (default: csi_dpll). The PicoSAT integration is experimental.
-help    Display this list of options.
-syntax  Choose the syntax to use.
         Options: foci, infix (default: try foci first then infix if it fails).
-round Try to round the coefficient to integer values. WARNING: has a limited precision.


Input language:
---------------
The language is similar to Foci.

query   ::  formula ; formula ; ... ; formula

formula :: '=' term term
         | '<=' term term
         | '&' '[' formula ... formula ']'
         | '|' '[' formula ... formula ']'
         | '~' formula

term    :: variable
         | '+' '[' term ... term ']'
         | '*' number term
         | function_symbol '[' term ... term ']'

'number' is an integer, floating point, or a ratio (number '/' number).

There is also an infix syntax:

query   ::  formula ; formula ; ... ; formula

formula :: term '=' term
         | term '<=' term
         | term '<' term
         | term '>=' term
         | term '>' term
         | formula '->' formula
         | formula '<->' formula
         | formula '&' formula
         | formula '|' formula
         | 'not' formula

term    :: variable
         | term '+' term
         | term '-' term
         | number '*' term
         | '-' term
         | function_symbol '(' term , ... , term ')'

(precedence levels are [->,<->], [&,|], [not]. They are parsed as
left-associative.)