diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2020-06-05 09:54:51 -0300 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-06-05 09:54:51 -0300 |
| commit | 80b0795702e71d54ed7c17ba809eebde628eb516 (patch) | |
| tree | d9950f742d4763b520185d4f27aa666d67509429 /test/regress | |
| parent | 60746dc3ac7806475b5b6dab03123df024bf613e (diff) | |
Printing FP values as binary or indexed BVs according to option (#4554)
Diffstat (limited to 'test/regress')
4 files changed, 5 insertions, 5 deletions
diff --git a/test/regress/regress0/printer/bv_consts_bin.smt2 b/test/regress/regress0/printer/bv_consts_bin.smt2 index e5c3c2824..f910c2c96 100644 --- a/test/regress/regress0/printer/bv_consts_bin.smt2 +++ b/test/regress/regress0/printer/bv_consts_bin.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --bv-print-consts-in-binary +; COMMAND-LINE: ; EXPECT: sat ; EXPECT: ((x #b0001)) (set-option :produce-models true) diff --git a/test/regress/regress0/printer/bv_consts_dec.smt2 b/test/regress/regress0/printer/bv_consts_dec.smt2 index 98d95e822..38337e8cf 100644 --- a/test/regress/regress0/printer/bv_consts_dec.smt2 +++ b/test/regress/regress0/printer/bv_consts_dec.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --no-bv-print-consts-in-binary +; COMMAND-LINE: --bv-print-consts-as-indexed-symbols ; EXPECT: sat ; EXPECT: ((x (_ bv1 4))) (set-option :produce-models true) diff --git a/test/regress/regress0/printer/empty_symbol_name.smt2 b/test/regress/regress0/printer/empty_symbol_name.smt2 index 46652bc24..41d1ffd84 100644 --- a/test/regress/regress0/printer/empty_symbol_name.smt2 +++ b/test/regress/regress0/printer/empty_symbol_name.smt2 @@ -1,5 +1,5 @@ ; EXPECT: sat -; EXPECT: ((|| (_ bv1 4))) +; EXPECT: ((|| #b0001)) (set-option :produce-models true) (set-logic QF_BV) (declare-const || (_ BitVec 4)) diff --git a/test/regress/regress0/printer/symbol_starting_w_digit.smt2 b/test/regress/regress0/printer/symbol_starting_w_digit.smt2 index 6a688a16f..ea13a65c2 100644 --- a/test/regress/regress0/printer/symbol_starting_w_digit.smt2 +++ b/test/regress/regress0/printer/symbol_starting_w_digit.smt2 @@ -1,6 +1,6 @@ ; EXPECT: sat -; EXPECT: ((|0_0| (_ bv1 4))) -; EXPECT: ((x (_ bv3 4))) +; EXPECT: ((|0_0| #b0001)) +; EXPECT: ((x #b0011)) (set-option :produce-models true) (set-logic QF_BV) (declare-const |0_0| (_ BitVec 4)) |