path: root/test/regress/regress1/strings/no-lazy-pp-quant.smt2

; COMMAND-LINE: --strings-exp --no-strings-lazy-pp
; EXPECT: sat
(set-info :smt-lib-version 2.5)
(set-logic ALL)
(set-info :status sat)
(declare-fun result () Int)
(declare-fun s () String)
(assert (! (not (= (str.to.int s) result)) :named a0))
(check-sat)