diff options
| author | Morgan Deters <mdeters@gmail.com> | 2011-04-20 11:19:50 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2011-04-20 11:19:50 +0000 |
| commit | 2499bd64a5ac688573ebbcd6114983f64a8094eb (patch) | |
| tree | 0d49608cf7c21298fbeb8606fa1943c96beb8652 /test/system | |
| parent | 5a98094e8eee680d4f489e901107dfc484a1679f (diff) | |
numerous bugfixes
Diffstat (limited to 'test/system')
| -rw-r--r-- | test/system/ouroborous.cpp | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/test/system/ouroborous.cpp b/test/system/ouroborous.cpp index abce24751..ac864d16b 100644 --- a/test/system/ouroborous.cpp +++ b/test/system/ouroborous.cpp @@ -127,6 +127,7 @@ int runTest() { runTestString("(= (f (f y)) x)"); runTestString("~BVPLUS(3, 0bin00, 0bin11)[2:1] = 0bin10", input::LANG_CVC4); + runTestString("~BVPLUS(3, BVMULT(2, 0bin01, 0bin11), 0bin11)[2:0]", input::LANG_CVC4); runTestString("a[x][y] = a[y][x]", input::LANG_CVC4); delete psr; |