summaryrefslogtreecommitdiff
path: root/test/regress/regress0/bool/issue6717-ite-rewrite.smt2
blob: 3f78823df7be9e51488e40354eb1cebef7d7c796 (plain) 
1
2
3
4
5
6
7

(set-logic ALL)
(declare-fun T () Bool)
(declare-fun v () String)
(assert (ite T T true))
(assert (or T (and (str.prefixof v "") (exists ((x Int)) (= "t" (str.substr v 0 x))))))
(set-info :status sat)
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback