MiniSmt
Home
Research
Teaching
Members
Events
News
MiniSmt
Home
Information
Web Interface
MiniSmt
1. Problem
Input a problem in
SMT-LIB format
.
(benchmark none :logic QF_NIA :extrafuns ((a Int)) :extrafuns ((b Int)) :assumption (> a 1000) :assumption (< a 2000) :assumption (= (+ b b) 8) :formula true )
2. Set Parameters
initial number of bits for arithmetic variables:
domain:
NAT
INT
RAT
REAL
timeout:
10 seconds
30 seconds
60 seconds
enable debug output
3. Run MiniSmt