MiniSmt (0.65)

MiniSmt is an SMT-solver for quantifier-free non-linear arithmetic. In contrast to most competitor tools it can find models over irrational domains.

Examples

Select example Example Example2 Example3

Load own example

Syntax highlighting

Plain text SMT

Tool input

(benchmark none :logic QF_NIA :extrafuns ((a Int)) :extrafuns ((b Int)) :assumption (> a 1000) :assumption (< a 2000) :assumption (= (+ b b) 8) :formula true )

Enable debug output

No Yes

Initial number of bits for arithmetic variables

Timeout

Select Strategy

NAT

INT

RAT

REAL