MiniSmt

MiniSmt

Input For input use the SMTLIB format. See http://combination.cs.uiowa.edu/smtlib/ for details.

Example:

(benchmark none
:logic QF_NIA
:extrafuns ((a Int) (b Int))
:extrapreds ((x))
:assumption (> a (ite x 2 b))
:formula (true)
)
( )
input Upload a file in the SMTLIB format. See http://combination.cs.uiowa.edu/smtlib/ for details.    
 
  NAT Allow natural numbers.   INT Allow integers.   RAT Allow rational numbers.   REAL Allow real numbers.