STP doesn't parse benchmark.

[TrevorHansen]

Tjark Weber has created a benchmark that STP doesn't currently parse:

https://groups.google.com/g/smt-lib/c/Lt4JeKpN3zM/m/doB9uy2jAgAJ?pli=1

(set-info :smt-lib-version 2.6)
(set-logic QF_BV)
(set-info :source |
	Constructed by Tjark Weber to test that the extensions defined
	in QF_BV are implemented according to their definition
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "check")
(set-info :status unsat)
; We use a (reasonably small) fixed bit width m > 0.
(declare-fun s () (_ BitVec 5))
(declare-fun t () (_ BitVec 5))
(declare-fun u () (_ BitVec 5))
(assert (not (and
; Bitvector constants
  (= (_ bv13 32) #b00000000000000000000000000001101)
; Bitwise operators
  (= (bvnand s t) (bvnot (bvand s t)))
  (= (bvnor s t) (bvnot (bvor s t)))
  (= (bvxor s t) (bvor (bvand s (bvnot t)) (bvand (bvnot s) t)))
  (= (bvxnor s t) (bvor (bvand s t) (bvand (bvnot s) (bvnot t))))
  (= (bvcomp s t) (bvand (bvxnor ((_ extract 4 4) s) ((_ extract 4 4) t))
                         (bvcomp ((_ extract 3 0) s) ((_ extract 3 0) t))))
  (= (bvxor s t u) (bvxor (bvxor s t) u))
; Arithmetic operators
  (= (bvsub s t) (bvadd s (bvneg t)))
  (= (bvsdiv s t) (let ((?msb_s ((_ extract 4 4) s))
                        (?msb_t ((_ extract 4 4) t)))
                    (ite (and (= ?msb_s #b0) (= ?msb_t #b0))
                         (bvudiv s t)
                    (ite (and (= ?msb_s #b1) (= ?msb_t #b0))
                         (bvneg (bvudiv (bvneg s) t))
                    (ite (and (= ?msb_s #b0) (= ?msb_t #b1))
                         (bvneg (bvudiv s (bvneg t)))
                         (bvudiv (bvneg s) (bvneg t)))))))
  (= (bvsrem s t) (let ((?msb_s ((_ extract 4 4) s))
                        (?msb_t ((_ extract 4 4) t)))
                    (ite (and (= ?msb_s #b0) (= ?msb_t #b0))
                         (bvurem s t)
                    (ite (and (= ?msb_s #b1) (= ?msb_t #b0))
                         (bvneg (bvurem (bvneg s) t))
                    (ite (and (= ?msb_s #b0) (= ?msb_t #b1))
                         (bvurem s (bvneg t))
                         (bvneg (bvurem (bvneg s) (bvneg t))))))))
  (= (bvsmod s t) (let ((?msb_s ((_ extract 4 4) s))
                        (?msb_t ((_ extract 4 4) t)))
                    (let ((abs_s (ite (= ?msb_s #b0) s (bvneg s)))
                          (abs_t (ite (= ?msb_t #b0) t (bvneg t))))
                      (let ((u (bvurem abs_s abs_t)))
                        (ite (= u (_ bv0 5))
                             u
                        (ite (and (= ?msb_s #b0) (= ?msb_t #b0))
                             u
                        (ite (and (= ?msb_s #b1) (= ?msb_t #b0))
                             (bvadd (bvneg u) t)
                        (ite (and (= ?msb_s #b0) (= ?msb_t #b1))
                             (bvadd u t)
                             (bvneg u)))))))))
  (= (bvule s t) (or (bvult s t) (= s t)))
  (= (bvugt s t) (bvult t s))
  (= (bvuge s t) (or (bvult t s) (= s t)))
  (= (bvslt s t) (or (and (= ((_ extract 4 4) s) #b1)
                          (= ((_ extract 4 4) t) #b0))
                     (and (= ((_ extract 4 4) s) ((_ extract 4 4) t))
                          (bvult s t))))
  (= (bvsle s t) (or (and (= ((_ extract 4 4) s) #b1)
                          (= ((_ extract 4 4) t) #b0))
                     (and (= ((_ extract 4 4) s) ((_ extract 4 4) t))
                          (bvule s t))))
  (= (bvsgt s t) (bvslt t s))
  (= (bvsge s t) (bvsle t s))
; Other operations
  (= (bvashr s t) (ite (= ((_ extract 4 4) s) #b0)
                       (bvlshr s t)
                       (bvnot (bvlshr (bvnot s) t))))
  (= ((_ repeat 1) t) t)
  (= ((_ repeat 2) t) (concat t ((_ repeat 1) t)))
  (= ((_ zero_extend 0) t) t)
  (= ((_ zero_extend 1) t) (concat ((_ repeat 1) #b0) t))
  (= ((_ sign_extend 0) t) t)
  (= ((_ sign_extend 1) t) (concat ((_ repeat 1) ((_ extract 4 4) t)) t))
  (= ((_ rotate_left 0) t) t)
  (= ((_ rotate_left 1) t) ((_ rotate_left 0)
                             (concat ((_ extract 3 0) t) ((_ extract 4 4) t))))

  (= ((_ rotate_right 0) t) t)
  (= ((_ rotate_right 1) t) ((_ rotate_right 0)
                              (concat ((_ extract 0 0) t) ((_ extract 4 1) t))))
)))
(check-sat)
(exit)

[aytey]

It seems that this is because the let is introduces a term with a name that already exists:

(set-logic QF_BV)
(declare-fun u () (_ BitVec 1))
(assert
 (let ((u (_ bv0 1)))
 (= (_ bv0 1) (_ bv0 1))))
(check-sat)
(exit)

if you rename the inner u to be anything that isn't u, the issue goes away. As it is, you get:

(error "syntax error: line 4 syntax error, unexpected TERMID_TOK, expecting STRING_TOK  token: u")

This parses with master on Z3, Boolector and CVC4.

[aytey]

Also doesn't work:

(set-logic QF_BV)
(declare-fun u () (_ BitVec 1))
(assert
 (let ((v (_ bv0 1)))
 (let ((v (_ bv0 1)))
 (= (_ bv0 1) (_ bv0 1)))))
(check-sat)
(exit)

Change here is to use the same let term twice in the same scope.

[aytey]

A naive implementation gives sat on this when it shouldn't:

(set-logic QF_BV)
(set-info :status unsat)
(declare-fun u () (_ BitVec 5))
(assert (not (= (_ bv0 5) (let ((u (_ bv0 5))) u))))
(check-sat)
(exit)

Keeping the file to test later

[TrevorHansen]

Unless someone beats me to it, I'll get this fixed for SMT-COMP (#399)

[msoos]

Is there a potential obvious fix here?

[aytey]

As far as I’m aware, nope. SMTLIB allows lets to shadow other symbols (and lets shadowing lets) — STP’s let manager cannot handle this.

At least, that’s my understanding for trying a 15 minute fix of this when the issue was first raised.

[aytey]

Basically, from my memory, symbols get resolved (by STP) “globally” first and then in the let manager.

If a let shadows a global symbol, STP resolves it globally and ignores the let-declared one.