[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