diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-03-12 14:43:42 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-03-12 14:43:42 -0500 |
commit | ec8ea8a9c993435c4c5e671b1beea45ac088de64 (patch) | |
tree | 600e29c93eddaee301f3ff294ff6f45a02089186 /test/regress | |
parent | f93a68fdf2b62a40dd74bdb04aafb60ea7f1a69a (diff) |
Move tuple/record update elimination from ppRewrite to expandDefinition (#2839)
Diffstat (limited to 'test/regress')
-rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/regress/regress0/datatypes/issue2838.cvc | 14 |
2 files changed, 15 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 6f147db3c..abec884c2 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -363,6 +363,7 @@ set(regress_0_tests regress0/datatypes/example-dailler-min.smt2 regress0/datatypes/is_test.smt2 regress0/datatypes/issue1433.smt2 + regress0/datatypes/issue2838.cvc regress0/datatypes/jsat-2.6.smt2 regress0/datatypes/model-subterms-min.smt2 regress0/datatypes/mutually-recursive.cvc diff --git a/test/regress/regress0/datatypes/issue2838.cvc b/test/regress/regress0/datatypes/issue2838.cvc new file mode 100644 index 000000000..95e1c898a --- /dev/null +++ b/test/regress/regress0/datatypes/issue2838.cvc @@ -0,0 +1,14 @@ +% EXPECT: sat +Ints_0 : ARRAY INT OF INT; +C : TYPE = [# i : INT #]; +CType : TYPE = ARRAY INT OF C; +C_0 : CType; +x : INT; +C_1 : CType = C_0 WITH [0].i := 2; + +ASSERT C_0[0].i = 0; +ASSERT C_0[1].i = 1; +ASSERT Ints_0[2] = Ints_0[0]; +ASSERT x = Ints_0[C_1[0].i]; +ASSERT x /= Ints_0[C_1[1].i]; +CHECKSAT; |