diff options
Diffstat (limited to 'test/regress/regress0')
| -rw-r--r-- | test/regress/regress0/strings/complement-simple.smt2 | 5 | ||||
| -rw-r--r-- | test/regress/regress0/strings/is_digit_simple.smt2 | 11 | ||||
| -rw-r--r-- | test/regress/regress0/strings/re_diff.smt2 | 11 | ||||
| -rw-r--r-- | test/regress/regress0/sygus/sygus-uf.sy | 4 |
4 files changed, 29 insertions, 2 deletions
diff --git a/test/regress/regress0/strings/complement-simple.smt2 b/test/regress/regress0/strings/complement-simple.smt2 new file mode 100644 index 000000000..c19699448 --- /dev/null +++ b/test/regress/regress0/strings/complement-simple.smt2 @@ -0,0 +1,5 @@ +(set-logic SLIA) +(set-info :status sat) +(declare-fun x () String) +(assert (str.in.re x (re.comp (str.to.re "ABC")))) +(check-sat) diff --git a/test/regress/regress0/strings/is_digit_simple.smt2 b/test/regress/regress0/strings/is_digit_simple.smt2 new file mode 100644 index 000000000..d95a22078 --- /dev/null +++ b/test/regress/regress0/strings/is_digit_simple.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --lang=smt2.6.1 +; EXPECT: sat +(set-logic ALL) +(set-info :status sat) + +(assert (str.is_digit "0")) +(assert (str.is_digit "7")) +(assert (not (str.is_digit "A"))) +(assert (not (str.is_digit ""))) + +(check-sat) diff --git a/test/regress/regress0/strings/re_diff.smt2 b/test/regress/regress0/strings/re_diff.smt2 new file mode 100644 index 000000000..d63731acb --- /dev/null +++ b/test/regress/regress0/strings/re_diff.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --lang=smt2.6.1 +; EXPECT: unsat +(set-logic ALL) +(set-info :status unsat) +(declare-fun x () String) +(declare-fun y () String) + +(assert (str.in_re x (re.diff (re.* (str.to_re "A")) re.none))) +(assert (or (not (str.in_re x (re.* (str.to_re "A")))) (str.in_re y (re.diff (re.* (str.to_re "B")) re.all)))) + +(check-sat) diff --git a/test/regress/regress0/sygus/sygus-uf.sy b/test/regress/regress0/sygus/sygus-uf.sy index 1b060637a..d506dd5b2 100644 --- a/test/regress/regress0/sygus/sygus-uf.sy +++ b/test/regress/regress0/sygus/sygus-uf.sy @@ -1,6 +1,6 @@ -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --sygus-out=status --uf-ho ; EXPECT: unsat -(set-logic LIA) +(set-logic UFLIA) (declare-fun uf (Int) Int) |