diff options
Diffstat (limited to 'test/regress/regress0')
| -rw-r--r-- | test/regress/regress0/strings/Makefile.am | 9 | ||||
| -rwxr-xr-x | test/regress/regress0/strings/unsound-0908.smt2 | 12 |
2 files changed, 17 insertions, 4 deletions
diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am index d521680d5..eb88df905 100644 --- a/test/regress/regress0/strings/Makefile.am +++ b/test/regress/regress0/strings/Makefile.am @@ -9,8 +9,8 @@ AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXE if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(LOG_COMPILER) \ - $(AM_LOG_FLAGS) $(LOG_FLAGS) + $(LOG_COMPILER) \ + $(AM_LOG_FLAGS) $(LOG_FLAGS) endif MAKEFLAGS = -k @@ -18,7 +18,7 @@ MAKEFLAGS = -k # These are run for all build profiles. # If a test shouldn't be run in e.g. competition mode, # put it below in "TESTS +=" -TESTS = \ +TESTS = \ at001.smt2 \ bug001.smt2 \ bug002.smt2 \ @@ -49,7 +49,8 @@ TESTS = \ loop007.smt2 \ loop008.smt2 \ loop009.smt2 \ - reloop.smt2 + reloop.smt2 \ + unsound-0908.smt2 FAILING_TESTS = diff --git a/test/regress/regress0/strings/unsound-0908.smt2 b/test/regress/regress0/strings/unsound-0908.smt2 new file mode 100755 index 000000000..cbaf5f5e4 --- /dev/null +++ b/test/regress/regress0/strings/unsound-0908.smt2 @@ -0,0 +1,12 @@ +(set-logic QF_S)
+(set-info :status sat)
+(declare-const x String)
+(assert (= (str.len x) 1))
+;(assert (= x "X"))
+(assert
+ (or
+ (not (> (str.len x) 1))
+ (= (str.at x 1) "Z")
+ )
+)
+(check-sat)
|