diff options
Diffstat (limited to 'test/regress/regress0/cvc3.userdoc.01.cvc')
| -rw-r--r-- | test/regress/regress0/cvc3.userdoc.01.cvc | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/test/regress/regress0/cvc3.userdoc.01.cvc b/test/regress/regress0/cvc3.userdoc.01.cvc index 7c89de4ac..e3e9aaf0a 100644 --- a/test/regress/regress0/cvc3.userdoc.01.cvc +++ b/test/regress/regress0/cvc3.userdoc.01.cvc @@ -1,31 +1,31 @@ % COMMAND-LINE: --incremental -% EXPECT: valid +% EXPECT: entailed QUERY 0bin0000111101010000 = 0hex0f50; -% EXPECT: valid +% EXPECT: entailed QUERY 0bin01@0bin0 = 0bin010; -% EXPECT: valid +% EXPECT: entailed QUERY 0bin0011[3:1] = 0bin001; -% EXPECT: valid +% EXPECT: entailed QUERY 0bin0011 << 3 = 0bin0011000; -% EXPECT: valid +% EXPECT: entailed QUERY 0bin1000 >> 3 = 0bin0001; -% EXPECT: valid +% EXPECT: entailed QUERY SX(0bin100, 5) = 0bin11100; -% EXPECT: valid +% EXPECT: entailed QUERY BVZEROEXTEND(0bin1,3) = 0bin0001; -% EXPECT: valid +% EXPECT: entailed QUERY BVREPEAT(0bin10,3) = 0bin101010; -% EXPECT: valid +% EXPECT: entailed QUERY BVROTL(0bin101,1) = 0bin011; -% EXPECT: valid +% EXPECT: entailed QUERY BVROTR(0bin101,1) = 0bin110; |