[SMT-LIB] Benchmark Conformance: log in AUFLIRA/nasa/

[cok@frontiernet.net]

----- "Nikolaj Bjorner" <nbjorner at microsoft.com> wrote:

> 
> While I support the SMT-LIB2 format (see my shameless plug:
> http://rise4fun.com/z3 ), I see its main priority as a low-level
> mostly 
> machine writeable/readable interchange format that as an added benefit
> is also human read/write-able.
> 
> Thanks,
> 
> Nikolaj
> 

Nikolaj - A nifty web-site but what is written on that web site is not (pure) SMT-LIB.
In particular it has

(declare-funs ((x Int) (y Int) (z Int)))
  (assert (>= (* 2 x) (+ y z)))
  (declare-funs ((f Int Int) (g Int Int Int)))
  (assert (< (f x) (g x x)))
  (assert (> (f y) (g x x)))
  check-sat
  (get-info model)
  push
  (assert (= x y))
  check-sat
  pop
  quit



  (declare-funs ((x Int) (y Int) (z Int))) - I've wanted the convenience of combining declarations also, but SMT-LIB does not currently have it.  Even better actually would be (declare-funs ((x  y z Int)))


  (get-info model) - Keywords used in get-info are supposed to start with a :, and :model is not one of them.  This is perhaps the not well-documented command get-model?

  push
  check-sat
  pop - As commands, these should all be in ()

  quit - should be (exit)

David