diff options
| author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2013-12-03 22:53:02 -0600 |
|---|---|---|
| committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2013-12-03 22:53:48 -0600 |
| commit | d8fd36d709c753671762e91720d8b2415b22bf08 (patch) | |
| tree | 06d754b882d784f9feac599a2658bd656e3ab358 /test/regress/regress0 | |
| parent | ce3b3b2c4aebff1cde3e7979c1a0eabb1c8dd695 (diff) | |
adds LB strategy
Diffstat (limited to 'test/regress/regress0')
| -rw-r--r-- | test/regress/regress0/strings/Makefile.am | 1 | ||||
| -rw-r--r-- | test/regress/regress0/strings/cardinality.smt2 | 2 | ||||
| -rw-r--r-- | test/regress/regress0/strings/fmf001.smt2 | 2 | ||||
| -rw-r--r-- | test/regress/regress0/strings/fmf002.smt2 | 2 | ||||
| -rw-r--r-- | test/regress/regress0/strings/str007.smt2 | 13 |
5 files changed, 17 insertions, 3 deletions
diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am index c98f37958..e24cbc565 100644 --- a/test/regress/regress0/strings/Makefile.am +++ b/test/regress/regress0/strings/Makefile.am @@ -26,6 +26,7 @@ TESTS = \ str004.smt2 \ str005.smt2 \ str006.smt2 \ + str007.smt2 \ fmf001.smt2 \ fmf002.smt2 \ model001.smt2 \ diff --git a/test/regress/regress0/strings/cardinality.smt2 b/test/regress/regress0/strings/cardinality.smt2 index 465ea0b5e..d64bc240e 100644 --- a/test/regress/regress0/strings/cardinality.smt2 +++ b/test/regress/regress0/strings/cardinality.smt2 @@ -1,7 +1,7 @@ (set-logic QF_S) (set-info :status unsat) -(set-option :str-alphabet-card 2) +(set-option :strings-alphabet-card 2) (declare-fun x () String) (declare-fun y () String) diff --git a/test/regress/regress0/strings/fmf001.smt2 b/test/regress/regress0/strings/fmf001.smt2 index a8874b59f..f5ed1c3fb 100644 --- a/test/regress/regress0/strings/fmf001.smt2 +++ b/test/regress/regress0/strings/fmf001.smt2 @@ -1,5 +1,5 @@ (set-logic QF_S)
-(set-option :fmf-strings true)
+(set-option :strings-fmf true)
(set-info :status sat)
(declare-fun x () String)
diff --git a/test/regress/regress0/strings/fmf002.smt2 b/test/regress/regress0/strings/fmf002.smt2 index 14f50c710..525fc152c 100644 --- a/test/regress/regress0/strings/fmf002.smt2 +++ b/test/regress/regress0/strings/fmf002.smt2 @@ -1,5 +1,5 @@ (set-logic QF_S)
-(set-option :fmf-strings true)
+(set-option :strings-fmf true)
(set-info :status sat)
(declare-fun x () String)
diff --git a/test/regress/regress0/strings/str007.smt2 b/test/regress/regress0/strings/str007.smt2 new file mode 100644 index 000000000..0ca2ec4c3 --- /dev/null +++ b/test/regress/regress0/strings/str007.smt2 @@ -0,0 +1,13 @@ +(set-logic QF_S)
+(set-info :status unsat)
+
+(declare-fun x () String)
+(declare-fun y () String)
+
+
+(assert (or (= x y) (= x y)))
+
+(assert (= (str.++ x "ba") (str.++ "ab" x)))
+(assert (= (str.++ y "ab") (str.++ "ab" y)))
+
+(check-sat)
|