diff options
| author | Andres Noetzli <noetzli@stanford.edu> | 2017-06-16 08:47:35 -0700 |
|---|---|---|
| committer | Andres Noetzli <noetzli@stanford.edu> | 2017-06-16 08:57:19 -0700 |
| commit | bb908d1df39b3064294e5da4813fbfbcb301646b (patch) | |
| tree | 5d9ec283717e86102e6722936ef71ca4056ab433 /test | |
| parent | 209b08887bc55349880b9ed6d858e23637267dee (diff) | |
Parse 'is', 'match' differently for non-DT input
In SMT 2.6, Datatypes are being introduced and they come
with testers (indexed identifier of the form (_ is c)) and
match expressions. This lead to failures in UFIDL
benchmarks in SMT-LIB because they declare the function
'is'. This commit changes the parser s.t. it does not
consider 'is' and 'match' special tokens unless the theory
of datatypes is enabled.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/regress0/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/declare-fun-is-match.smt2 | 9 |
2 files changed, 11 insertions, 1 deletions
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 1d2cc9f45..98be91454 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -68,7 +68,8 @@ SMT2_TESTS = \ hung10_itesdk_output2.smt2 \ hung10_itesdk_output1.smt2 \ hung13sdk_output2.smt2 \ - declare-funs.smt2 + declare-funs.smt2 \ + declare-fun-is-match.smt2 # Regression tests for PL inputs CVC_TESTS = \ diff --git a/test/regress/regress0/declare-fun-is-match.smt2 b/test/regress/regress0/declare-fun-is-match.smt2 new file mode 100644 index 000000000..d9387208f --- /dev/null +++ b/test/regress/regress0/declare-fun-is-match.smt2 @@ -0,0 +1,9 @@ +; EXPECT: sat +(set-info :smt-lib-version 2.6) +(set-logic UFIDL) +(set-info :status sat) +(declare-fun match (Int Int) Int) +(declare-fun is (Int Int) Int) +(assert (= match is)) +(check-sat) +(exit) |