[SMT-LIB] New SMT-LIB release for SMT-COMP 2011---includes fixes, additions
cok at frontiernet.net
cok at frontiernet.net
Fri May 27 06:35:46 EDT 2011
Morgan,
The expression (> tx_conta_99 104) in QF_UFIDL does not match the rules:
"Closed quantifier-free formulas with atoms of the form:
- p
- (op (- x y) n),
- (op (- x y) (- n)),
- (op x y), or
where
- p is a variable or free constant symbol of sort Bool,
- op is <, <=, >, >=, =, or distinct,
- x, y are free constant symbols of sort Ints,
- n is a numeral.
"
though arguably it is the rules that should be changed.
- David
More information about the SMT-LIB
mailing list