diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-10-15 17:58:35 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-10-15 17:58:35 +0200 |
| commit | 8914ff73f09a0e0b4c3bc40107c9345c8ea43760 (patch) | |
| tree | d22fac337ff105dd35c6cd65b18b928928205bc5 /test | |
| parent | 614080814375998f494adc839484f455b31a5f43 (diff) | |
Fix congruence check in strings, fixes bug 686.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/regress0/strings/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/strings/bug686dd.smt2 | 13 |
2 files changed, 15 insertions, 1 deletions
diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am index 45a7fb802..962340a91 100644 --- a/test/regress/regress0/strings/Makefile.am +++ b/test/regress/regress0/strings/Makefile.am @@ -69,7 +69,8 @@ TESTS = \ kaluza-fl.smt2 \ norn-ab.smt2 \ idof-rewrites.smt2 \ - bug682.smt2 + bug682.smt2 \ + bug686dd.smt2 FAILING_TESTS = diff --git a/test/regress/regress0/strings/bug686dd.smt2 b/test/regress/regress0/strings/bug686dd.smt2 new file mode 100644 index 000000000..7db4b86f0 --- /dev/null +++ b/test/regress/regress0/strings/bug686dd.smt2 @@ -0,0 +1,13 @@ +(set-logic UFDTSLIA)
+(set-info :status sat)
+
+(declare-datatypes () ( (T (TC (TCb String))) ) )
+
+(declare-fun root5 () String)
+(declare-fun root6 () T)
+
+(assert (and
+(str.in.re root5 (re.loop (re.range "0" "9") 4 4) )
+(str.in.re (TCb root6) (re.loop (re.range "0" "9") 4 4) )
+) )
+(check-sat)
|