Commit 5e4d2a69 authored by Mathias Preiner's avatar Mathias Preiner
Browse files

Move benchmarks from pending repository.

parent 4ef860dd
(set-info :smt-lib-version 2.6)
(set-logic QF_SLIA)
(set-info :source |
Generated by: Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukáš Holík, Ahmed Rezine, Philipp Rümmer, Jari Stenman
Generated on: 2015-03-09
Generator: Eldarica
Application: CEGAR based model checking for string programs
Target solver: Norn
Publication: "String constraints for verification" by P.A. Abdulla, M.F. Atig, Y.F. Chen, L. Holík, A. Rezine, P. Rümmer, and J. Stenman, CAV 2014.
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun var_0 () String)
(declare-fun var_1 () String)
(declare-fun var_2 () String)
(declare-fun var_3 () String)
(declare-fun var_4 () String)
(declare-fun var_5 () String)
(declare-fun var_6 () String)
(declare-fun var_7 () String)
(declare-fun var_8 () String)
(declare-fun var_9 () String)
(declare-fun var_10 () String)
(declare-fun var_11 () String)
(declare-fun var_12 () String)
(assert (str.in_re var_1 (re.* (re.union (str.to_re "a") (str.to_re "b")))))
(check-sat)
(exit)
(set-info :smt-lib-version 2.6)
(set-logic QF_SLIA)
(set-info :source |
Generated by: Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukáš Holík, Ahmed Rezine, Philipp Rümmer, Jari Stenman
Generated on: 2015-03-09
Generator: Eldarica
Application: CEGAR based model checking for string programs
Target solver: Norn
Publication: "String constraints for verification" by P.A. Abdulla, M.F. Atig, Y.F. Chen, L. Holík, A. Rezine, P. Rümmer, and J. Stenman, CAV 2014.
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun var_0 () String)
(declare-fun var_1 () String)
(declare-fun var_2 () String)
(declare-fun var_3 () String)
(declare-fun var_4 () String)
(declare-fun var_5 () String)
(declare-fun var_6 () String)
(declare-fun var_7 () String)
(declare-fun var_8 () String)
(declare-fun var_9 () String)
(declare-fun var_10 () String)
(declare-fun var_11 () String)
(declare-fun var_12 () String)
(assert (and (and (and (and (and (<= (+ (str.len var_2) (- 8) ) 0 ) (<= 0 (+ (str.len var_2) (- 8) ))) (and (<= (+ (+ (+ (str.len var_3) (str.len var_4)) (* (- 1) (str.len var_0))) 8 ) 0 ) (<= 0 (+ (+ (+ (str.len var_3) (str.len var_4)) (* (- 1) (str.len var_0))) 8 )))) (and (<= (+ (+ (str.len var_1) (* (- 1) (str.len var_4))) (- 8) ) 0 ) (<= 0 (+ (+ (str.len var_1) (* (- 1) (str.len var_4))) (- 8) )))) (<= 0 (+ (+ (* (- 1) (str.len var_4)) (str.len var_0)) (- 8) ))) (<= 0 (str.len var_4))))
(check-sat)
(exit)
(set-info :smt-lib-version 2.6)
(set-logic QF_SLIA)
(set-info :source |
Generated by: Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukáš Holík, Ahmed Rezine, Philipp Rümmer, Jari Stenman
Generated on: 2015-03-09
Generator: Eldarica
Application: CEGAR based model checking for string programs
Target solver: Norn
Publication: "String constraints for verification" by P.A. Abdulla, M.F. Atig, Y.F. Chen, L. Holík, A. Rezine, P. Rümmer, and J. Stenman, CAV 2014.
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun var_0 () String)
(declare-fun var_1 () String)
(declare-fun var_2 () String)
(declare-fun var_3 () String)
(declare-fun var_4 () String)
(declare-fun var_5 () String)
(declare-fun var_6 () String)
(declare-fun var_7 () String)
(declare-fun var_8 () String)
(declare-fun var_9 () String)
(declare-fun var_10 () String)
(declare-fun var_11 () String)
(declare-fun var_12 () String)
(assert (str.in_re "" (re.* (re.range "a" "u"))))
(assert (str.in_re var_1 (re.* (re.union (str.to_re "a") (str.to_re "b")))))
(assert (str.in_re var_1 (re.* (re.range "a" "u"))))
(check-sat)
(exit)
(set-info :smt-lib-version 2.6)
(set-logic QF_SLIA)
(set-info :source |
Generated by: Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukáš Holík, Ahmed Rezine, Philipp Rümmer, Jari Stenman
Generated on: 2015-03-09
Generator: Eldarica
Application: CEGAR based model checking for string programs
Target solver: Norn
Publication: "String constraints for verification" by P.A. Abdulla, M.F. Atig, Y.F. Chen, L. Holík, A. Rezine, P. Rümmer, and J. Stenman, CAV 2014.
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun var_0 () String)
(declare-fun var_1 () String)
(declare-fun var_2 () String)
(declare-fun var_3 () String)
(declare-fun var_4 () String)
(declare-fun var_5 () String)
(declare-fun var_6 () String)
(declare-fun var_7 () String)
(declare-fun var_8 () String)
(declare-fun var_9 () String)
(declare-fun var_10 () String)
(declare-fun var_11 () String)
(declare-fun var_12 () String)
(assert (str.in_re var_1 (re.* (re.range "a" "u"))))
(assert (str.in_re var_1 (str.to_re "")))
(assert (not (str.in_re "" re.none)))
(assert (not (str.in_re var_1 (re.* (re.union (re.union (str.to_re "a") (str.to_re "b")) (str.to_re "c"))))))
(check-sat)
(exit)
(set-info :smt-lib-version 2.6)
(set-logic QF_SLIA)
(set-info :source |
Generated by: Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukáš Holík, Ahmed Rezine, Philipp Rümmer, Jari Stenman
Generated on: 2015-03-09
Generator: Eldarica
Application: CEGAR based model checking for string programs
Target solver: Norn
Publication: "String constraints for verification" by P.A. Abdulla, M.F. Atig, Y.F. Chen, L. Holík, A. Rezine, P. Rümmer, and J. Stenman, CAV 2014.
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun var_0 () String)
(declare-fun var_1 () String)
(declare-fun var_2 () String)
(declare-fun var_3 () String)
(declare-fun var_4 () String)
(declare-fun var_5 () String)
(declare-fun var_6 () String)
(declare-fun var_7 () String)
(declare-fun var_8 () String)
(declare-fun var_9 () String)
(declare-fun var_10 () String)
(declare-fun var_11 () String)
(declare-fun var_12 () String)
(assert (str.in_re (str.++ var_3 "z" var_4 ) (re.* (str.to_re "z"))))
(assert (str.in_re var_4 (re.* (re.range "a" "u"))))
(assert (str.in_re var_3 (re.* (re.range "a" "u"))))
(assert (not (str.in_re var_3 (str.to_re ""))))
(assert (<= 0 (str.len var_3)))
(check-sat)
(exit)
(set-info :smt-lib-version 2.6)
(set-logic QF_SLIA)
(set-info :source |
Generated by: Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukáš Holík, Ahmed Rezine, Philipp Rümmer, Jari Stenman
Generated on: 2015-03-09
Generator: Eldarica
Application: CEGAR based model checking for string programs
Target solver: Norn
Publication: "String constraints for verification" by P.A. Abdulla, M.F. Atig, Y.F. Chen, L. Holík, A. Rezine, P. Rümmer, and J. Stenman, CAV 2014.
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun var_0 () String)
(declare-fun var_1 () String)
(declare-fun var_2 () String)
(declare-fun var_3 () String)
(declare-fun var_4 () String)
(declare-fun var_5 () String)
(declare-fun var_6 () String)
(declare-fun var_7 () String)
(declare-fun var_8 () String)
(declare-fun var_9 () String)
(declare-fun var_10 () String)
(declare-fun var_11 () String)
(declare-fun var_12 () String)
(assert (str.in_re "" (re.* (re.range "a" "u"))))
(assert (str.in_re var_4 (re.* (re.range "a" "u"))))
(assert (str.in_re var_4 (re.* (re.union (str.to_re "a") (str.to_re "b")))))
(assert (not (str.in_re (str.++ var_4 "z" ) (re.* (str.to_re "z")))))
(check-sat)
(exit)
(set-info :smt-lib-version 2.6)
(set-logic QF_SLIA)
(set-info :source |
Generated by: Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukáš Holík, Ahmed Rezine, Philipp Rümmer, Jari Stenman
Generated on: 2015-03-09
Generator: Eldarica
Application: CEGAR based model checking for string programs
Target solver: Norn
Publication: "String constraints for verification" by P.A. Abdulla, M.F. Atig, Y.F. Chen, L. Holík, A. Rezine, P. Rümmer, and J. Stenman, CAV 2014.
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun var_0 () String)
(declare-fun var_1 () String)
(declare-fun var_2 () String)
(declare-fun var_3 () String)
(declare-fun var_4 () String)
(declare-fun var_5 () String)
(declare-fun var_6 () String)
(declare-fun var_7 () String)
(declare-fun var_8 () String)
(declare-fun var_9 () String)
(declare-fun var_10 () String)
(declare-fun var_11 () String)
(declare-fun var_12 () String)
(assert (str.in_re (str.++ var_3 "z" var_4 ) (re.* (re.union (str.to_re "z") (re.union (re.union (str.to_re "a") (str.to_re "b")) (str.to_re "c"))))))
(assert (str.in_re var_4 (re.* (re.range "a" "u"))))
(assert (str.in_re var_3 (re.* (re.range "a" "u"))))
(assert (not (str.in_re var_3 (str.to_re ""))))
(assert (<= 0 (str.len var_3)))
(check-sat)
(exit)
(set-info :smt-lib-version 2.6)
(set-logic QF_SLIA)
(set-info :source |
Generated by: Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukáš Holík, Ahmed Rezine, Philipp Rümmer, Jari Stenman
Generated on: 2015-03-09
Generator: Eldarica
Application: CEGAR based model checking for string programs
Target solver: Norn
Publication: "String constraints for verification" by P.A. Abdulla, M.F. Atig, Y.F. Chen, L. Holík, A. Rezine, P. Rümmer, and J. Stenman, CAV 2014.
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun var_0 () String)
(declare-fun var_1 () String)
(declare-fun var_2 () String)
(declare-fun var_3 () String)
(declare-fun var_4 () String)
(declare-fun var_5 () String)
(declare-fun var_6 () String)
(declare-fun var_7 () String)
(declare-fun var_8 () String)
(declare-fun var_9 () String)
(declare-fun var_10 () String)
(declare-fun var_11 () String)
(declare-fun var_12 () String)
(assert (str.in_re (str.++ var_3 "z" var_4 ) (re.* (re.union (str.to_re "z") (re.union (re.union (str.to_re "a") (str.to_re "b")) (str.to_re "c"))))))
(assert (str.in_re var_4 (re.* (re.range "a" "u"))))
(assert (str.in_re var_3 (re.* (re.range "a" "u"))))
(assert (not (str.in_re var_3 (re.* (re.union (re.union (str.to_re "a") (str.to_re "b")) (str.to_re "c"))))))
(assert (<= 0 (str.len var_3)))
(check-sat)
(exit)
(set-info :smt-lib-version 2.6)
(set-logic QF_SLIA)
(set-info :source |
Generated by: Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukáš Holík, Ahmed Rezine, Philipp Rümmer, Jari Stenman
Generated on: 2015-03-09
Generator: Eldarica
Application: CEGAR based model checking for string programs
Target solver: Norn
Publication: "String constraints for verification" by P.A. Abdulla, M.F. Atig, Y.F. Chen, L. Holík, A. Rezine, P. Rümmer, and J. Stenman, CAV 2014.
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun var_0 () String)
(declare-fun var_1 () String)
(declare-fun var_2 () String)
(declare-fun var_3 () String)
(declare-fun var_4 () String)
(declare-fun var_5 () String)
(declare-fun var_6 () String)
(declare-fun var_7 () String)
(declare-fun var_8 () String)
(declare-fun var_9 () String)
(declare-fun var_10 () String)
(declare-fun var_11 () String)
(declare-fun var_12 () String)
(assert (str.in_re "" (re.* (re.range "a" "u"))))
(assert (str.in_re var_4 (re.* (re.range "a" "u"))))
(assert (str.in_re var_4 (re.* (re.union (str.to_re "a") (str.to_re "b")))))
(assert (not (str.in_re (str.++ var_4 "z" ) (re.* (re.union (str.to_re "z") (re.union (re.union (str.to_re "a") (str.to_re "b")) (str.to_re "c")))))))
(check-sat)
(exit)
(set-info :smt-lib-version 2.6)
(set-logic QF_SLIA)
(set-info :source |
Generated by: Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukáš Holík, Ahmed Rezine, Philipp Rümmer, Jari Stenman
Generated on: 2015-03-09
Generator: Eldarica
Application: CEGAR based model checking for string programs
Target solver: Norn
Publication: "String constraints for verification" by P.A. Abdulla, M.F. Atig, Y.F. Chen, L. Holík, A. Rezine, P. Rümmer, and J. Stenman, CAV 2014.
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun var_0 () String)
(declare-fun var_1 () String)
(declare-fun var_2 () String)
(declare-fun var_3 () String)
(declare-fun var_4 () String)
(declare-fun var_5 () String)
(declare-fun var_6 () String)
(declare-fun var_7 () String)
(declare-fun var_8 () String)
(declare-fun var_9 () String)
(declare-fun var_10 () String)
(declare-fun var_11 () String)
(declare-fun var_12 () String)
(assert (<= 0 (str.len var_0)))
(check-sat)
(exit)
(set-info :smt-lib-version 2.6)
(set-logic QF_SLIA)
(set-info :source |
Generated by: Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukáš Holík, Ahmed Rezine, Philipp Rümmer, Jari Stenman
Generated on: 2015-03-09
Generator: Eldarica
Application: CEGAR based model checking for string programs
Target solver: Norn
Publication: "String constraints for verification" by P.A. Abdulla, M.F. Atig, Y.F. Chen, L. Holík, A. Rezine, P. Rümmer, and J. Stenman, CAV 2014.
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun var_0 () String)
(declare-fun var_1 () String)
(declare-fun var_2 () String)
(declare-fun var_3 () String)
(declare-fun var_4 () String)
(declare-fun var_5 () String)
(declare-fun var_6 () String)
(declare-fun var_7 () String)
(declare-fun var_8 () String)
(declare-fun var_9 () String)
(declare-fun var_10 () String)
(declare-fun var_11 () String)
(declare-fun var_12 () String)
(assert (not (str.in_re var_0 (re.* (re.range "a" "u")))))
(assert (<= 0 (str.len var_0)))
(check-sat)
(exit)
(set-info :smt-lib-version 2.6)
(set-logic QF_SLIA)
(set-info :source |
Generated by: Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukáš Holík, Ahmed Rezine, Philipp Rümmer, Jari Stenman
Generated on: 2015-03-09
Generator: Eldarica
Application: CEGAR based model checking for string programs
Target solver: Norn
Publication: "String constraints for verification" by P.A. Abdulla, M.F. Atig, Y.F. Chen, L. Holík, A. Rezine, P. Rümmer, and J. Stenman, CAV 2014.
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun var_0 () String)
(declare-fun var_1 () String)
(declare-fun var_2 () String)
(declare-fun var_3 () String)
(declare-fun var_4 () String)
(declare-fun var_5 () String)
(declare-fun var_6 () String)
(declare-fun var_7 () String)
(declare-fun var_8 () String)
(declare-fun var_9 () String)
(declare-fun var_10 () String)
(declare-fun var_11 () String)
(declare-fun var_12 () String)
(assert (str.in_re var_4 (re.* (re.union (str.to_re "a") (str.to_re "b")))))
(assert (not (str.in_re (str.++ var_4 "z" ) (re.* (re.union (str.to_re "z") (re.union (re.union (str.to_re "a") (str.to_re "b")) (str.to_re "c")))))))
(check-sat)
(exit)
(set-info :smt-lib-version 2.6)
(set-logic QF_SLIA)
(set-info :source |
Generated by: Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukáš Holík, Ahmed Rezine, Philipp Rümmer, Jari Stenman
Generated on: 2015-03-09
Generator: Eldarica
Application: CEGAR based model checking for string programs
Target solver: Norn
Publication: "String constraints for verification" by P.A. Abdulla, M.F. Atig, Y.F. Chen, L. Holík, A. Rezine, P. Rümmer, and J. Stenman, CAV 2014.
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun var_0 () String)
(declare-fun var_1 () String)
(declare-fun var_2 () String)
(declare-fun var_3 () String)
(declare-fun var_4 () String)
(declare-fun var_5 () String)
(declare-fun var_6 () String)
(declare-fun var_7 () String)
(declare-fun var_8 () String)
(declare-fun var_9 () String)
(declare-fun var_10 () String)
(declare-fun var_11 () String)
(declare-fun var_12 () String)
(assert (str.in_re var_1 (re.* (re.union (str.to_re "a") (str.to_re "b")))))
(assert (not (str.in_re "" (re.* (re.range "a" "u")))))
(check-sat)
(exit)
(set-info :smt-lib-version 2.6)
(set-logic QF_SLIA)
(set-info :source |
Generated by: Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukáš Holík, Ahmed Rezine, Philipp Rümmer, Jari Stenman
Generated on: 2015-03-09
Generator: Eldarica
Application: CEGAR based model checking for string programs
Target solver: Norn
Publication: "String constraints for verification" by P.A. Abdulla, M.F. Atig, Y.F. Chen, L. Holík, A. Rezine, P. Rümmer, and J. Stenman, CAV 2014.
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun var_0 () String)
(declare-fun var_1 () String)
(declare-fun var_2 () String)
(declare-fun var_3 () String)
(declare-fun var_4 () String)
(declare-fun var_5 () String)
(declare-fun var_6 () String)
(declare-fun var_7 () String)
(declare-fun var_8 () String)
(declare-fun var_9 () String)
(declare-fun var_10 () String)
(declare-fun var_11 () String)
(declare-fun var_12 () String)
(assert (str.in_re "" (re.* (re.range "a" "u"))))
(assert (str.in_re var_1 (re.* (re.union (str.to_re "a") (str.to_re "b")))))
(assert (not (str.in_re var_1 (re.* (re.range "a" "u")))))
(check-sat)
(exit)
(set-info :smt-lib-version 2.6)
(set-logic QF_SLIA)
(set-info :source |
Generated by: Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukáš Holík, Ahmed Rezine, Philipp Rümmer, Jari Stenman
Generated on: 2015-03-09
Generator: Eldarica
Application: CEGAR based model checking for string programs
Target solver: Norn
Publication: "String constraints for verification" by P.A. Abdulla, M.F. Atig, Y.F. Chen, L. Holík, A. Rezine, P. Rümmer, and J. Stenman, CAV 2014.
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun var_0 () String)
(declare-fun var_1 () String)
(declare-fun var_2 () String)
(declare-fun var_3 () String)
(declare-fun var_4 () String)
(declare-fun var_5 () String)
(declare-fun var_6 () String)
(declare-fun var_7 () String)
(declare-fun var_8 () String)
(declare-fun var_9 () String)
(declare-fun var_10 () String)
(declare-fun var_11 () String)
(declare-fun var_12 () String)
(assert (not (str.in_re (str.++ var_2 var_3 ) (re.* (re.range "a" "u")))))
(assert (and (and (and (and (and (<= (+ (str.len var_3) (- 8) ) 0 ) (<= 0 (+ (str.len var_3) (- 8) ))) (and (<= (+ (+ (+ (str.len var_4) (str.len var_2)) (* (- 1) (str.len var_0))) 8 ) 0 ) (<= 0 (+ (+ (+ (str.len var_4) (str.len var_2)) (* (- 1) (str.len var_0))) 8 )))) (and (<= (+ (+ (str.len var_1) (* (- 1) (str.len var_2))) (- 8) ) 0 ) (<= 0 (+ (+ (str.len var_1) (* (- 1) (str.len var_2))) (- 8) )))) (<= 0 (+ (+ (* (- 1) (str.len var_2)) (str.len var_0)) (- 8) ))) (<= 0 (str.len var_2))))
(check-sat)
(exit)
(set-info :smt-lib-version 2.6)
(set-logic QF_SLIA)
(set-info :source |
Generated by: Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukáš Holík, Ahmed Rezine, Philipp Rümmer, Jari Stenman
Generated on: 2015-03-09
Generator: Eldarica
Application: CEGAR based model checking for string programs
Target solver: Norn
Publication: "String constraints for verification" by P.A. Abdulla, M.F. Atig, Y.F. Chen, L. Holík, A. Rezine, P. Rümmer, and J. Stenman, CAV 2014.
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun var_0 () String)
(declare-fun var_1 () String)
(declare-fun var_2 () String)
(declare-fun var_3 () String)
(declare-fun var_4 () String)
(declare-fun var_5 () String)
(declare-fun var_6 () String)
(declare-fun var_7 () String)
(declare-fun var_8 () String)
(declare-fun var_9 () String)
(declare-fun var_10 () String)
(declare-fun var_11 () String)
(declare-fun var_12 () String)
(assert (str.in_re (str.++ var_5 var_6 var_7 "z" var_5 ) (re.* (re.union (str.to_re "z") (re.union (re.union (str.to_re "a") (str.to_re "b")) (str.to_re "c"))))))
(assert (str.in_re var_5 (re.* (re.range "a" "u"))))
(assert (str.in_re (str.++ var_5 var_6 var_7 ) (re.* (re.range "a" "u"))))
(assert (and (and (and (and (and (<= (+ (str.len var_6) (- 8) ) 0 ) (<= 0 (+ (str.len var_6) (- 8) ))) (and (<= (+ (+ (+ (str.len var_7) (str.len var_5)) (* (- 1) (str.len var_2))) 8 ) 0 ) (<= 0 (+ (+ (+ (str.len var_7) (str.len var_5)) (* (- 1) (str.len var_2))) 8 )))) (and (<= (+ (+ (str.len var_3) (* (- 1) (str.len var_5))) (- 8) ) 0 ) (<= 0 (+ (+ (str.len var_3) (* (- 1) (str.len var_5))) (- 8) )))) (<= 0 (+ (+ (* (- 1) (str.len var_5)) (str.len var_2)) (- 8) ))) (<= 0 (str.len var_5))))
(check-sat)
(exit)
(set-info :smt-lib-version 2.6)
(set-logic QF_SLIA)
(set-info :source |
Generated by: Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukáš Holík, Ahmed Rezine, Philipp Rümmer, Jari Stenman
Generated on: 2015-03-09
Generator: Eldarica
Application: CEGAR based model checking for string programs
Target solver: Norn
Publication: "String constraints for verification" by P.A. Abdulla, M.F. Atig, Y.F. Chen, L. Holík, A. Rezine, P. Rümmer, and J. Stenman, CAV 2014.
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun var_0 () String)
(declare-fun var_1 () String)
(declare-fun var_2 () String)
(declare-fun var_3 () String)
(declare-fun var_4 () String)
(declare-fun var_5 () String)
(declare-fun var_6 () String)
(declare-fun var_7 () String)
(declare-fun var_8 () String)
(declare-fun var_9 () String)
(declare-fun var_10 () String)
(declare-fun var_11 () String)
(declare-fun var_12 () String)
(assert (str.in_re (str.++ var_10 var_11 var_12 "z" var_10 ) (re.* (re.union (str.to_re "z") (re.union (re.union (str.to_re "a") (str.to_re "b")) (str.to_re "c"))))))
(assert (str.in_re var_10 (re.* (re.range "a" "u"))))
(assert (str.in_re (str.++ var_10 var_11 var_12 ) (re.* (re.range "a" "u"))))
(assert (not (str.in_re (str.++ var_10 var_11 "c" var_12 "z" var_10 var_11 ) (re.* (re.union (str.to_re "z") (re.union (re.union (str.to_re "a") (str.to_re "b")) (str.to_re "c")))))))
(assert (and (and (and (and (and (<= (+ (str.len var_11) (- 8) ) 0 ) (<= 0 (+ (str.len var_11) (- 8) ))) (and (<= (+ (+ (+ (str.len var_12) (str.len var_10)) (* (- 1) (str.len var_5))) 8 ) 0 ) (<= 0 (+ (+ (+ (str.len var_12) (str.len var_10)) (* (- 1) (str.len var_5))) 8 )))) (and (<= (+ (+ (str.len var_8) (* (- 1) (str.len var_10))) (- 8) ) 0 ) (<= 0 (+ (+ (str.len var_8) (* (- 1) (str.len var_10))) (- 8) )))) (<= 0 (+ (+ (* (- 1) (str.len var_10)) (str.len var_5)) (- 8) ))) (<= 0 (str.len var_10))))
(check-sat)
(exit)
(set-info :smt-lib-version 2.6)
(set-logic QF_SLIA)
(set-info :source |
Generated by: Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukáš Holík, Ahmed Rezine, Philipp Rümmer, Jari Stenman
Generated on: 2015-03-09
Generator: Eldarica
Application: CEGAR based model checking for string programs
Target solver: Norn
Publication: "String constraints for verification" by P.A. Abdulla, M.F. Atig, Y.F. Chen, L. Holík, A. Rezine, P. Rümmer, and J. Stenman, CAV 2014.
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun var_0 () String)
(declare-fun var_1 () String)
(declare-fun var_2 () String)
(declare-fun var_3 () String)
(declare-fun var_4 () String)
(declare-fun var_5 () String)
(declare-fun var_6 () String)
(declare-fun var_7 () String)
(declare-fun var_8 () String)
(declare-fun var_9 () String)
(declare-fun var_10 () String)
(declare-fun var_11 () String)
(declare-fun var_12 () String)
(assert (str.in_re (str.++ var_5 var_6 var_7 "z" var_5 ) (re.* (re.union (str.to_re "z") (re.union (re.union (str.to_re "a") (str.to_re "b")) (str.to_re "c"))))))
(assert (str.in_re var_5 (re.* (re.range "a" "u"))))
(assert (str.in_re (str.++ var_5 var_6 var_7 ) (re.* (re.range "a" "u"))))
(assert (not (str.in_re (str.++ var_5 var_6 ) (re.* (re.range "a" "u")))))
(assert (and (and (and (and (and (<= (+ (str.len var_6) (- 8) ) 0 ) (<= 0 (+ (str.len var_6) (- 8) ))) (and (<= (+ (+ (+ (str.len var_7) (str.len var_5)) (* (- 1) (str.len var_2))) 8 ) 0 ) (<= 0 (+ (+ (+ (str.len var_7) (str.len var_5)) (* (- 1) (str.len var_2))) 8 )))) (and (<= (+ (+ (str.len var_3) (* (- 1) (str.len var_5))) (- 8) ) 0 ) (<= 0 (+ (+ (str.len var_3) (* (- 1) (str.len var_5))) (- 8) )))) (<= 0 (+ (+ (* (- 1) (str.len var_5)) (str.len var_2)) (- 8) ))) (<= 0 (str.len var_5))))
(check-sat)
(exit)
(set-info :smt-lib-version 2.6)
(set-logic QF_SLIA)
(set-info :source |