blob: 2ffe8a7a729084e5cab549b10a02a181c90c91ae (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
(set-info :smt-lib-version 2.6)
(set-logic QF_SLIA)
(set-info :source |
Generated by: Quang Loc Le
Generated on: 2018-10-22
Application: Word equations in a decidable fragment
Target solver: Kepler_22
Publication: "A decision procedure for string logic with quadratic equations, regular expressions and length constraints" by Q.L. Le and M. He, APLAS 2018.
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "crafted")
(set-info :status unsat)
(declare-fun x1 () String )
(declare-fun x2 () String )
(declare-fun z () String )
(declare-fun t () String )
(assert ( =( str.++( str.++( str.++ x1 "abc" ) x2 ) z ) ( str.++( str.++( str.++ x2 "bab" ) x1 ) t ) ) )
(check-sat)
(exit)
|
