test/regress/regress1/quantifiers/issue2970-string-var-elim.smt2


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15

; COMMAND-LINE: --strings-exp
(set-logic ALL)
(set-info :status unsat)
(declare-fun s () String)
(declare-fun t () String)
(assert (! 
 (forall ((t1 String) (t2 String))
  (=> (= (str.++ t1 t2) t) (= (= t1 s) false))
  )
  :named a1))
(assert (! 
 (not (= (str.prefixof s t) false)) :named a0))


(check-sat)