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 /NEWS | |
parent | 60746dc3ac7806475b5b6dab03123df024bf613e (diff) |
Printing FP values as binary or indexed BVs according to option (#4554)
Diffstat (limited to 'NEWS')
-rw-r--r-- | NEWS | 7 |
1 files changed, 7 insertions, 0 deletions
@@ -9,6 +9,13 @@ Changes: `Result::Entailment` along with corresponding changes to the enum values. * Java API change: The name of CVC4's package is now `edu.stanford.CVC4` instead of `edu.nyu.acsys.CVC4`. +* Printing of BV constants: previously CVC4 would print BV constant + values as indexed symbols by default and in binary notation with the + option --bv-print-consts-in-binary. To be SMT-LIB compliant the + default behavior is now to print BV constant values in binary + notation and as indexed symbols with the new option + --bv-print-consts-as-indexed-symbols. The option + --bv-print-consts-in-binary has been removed. Changes since 1.6 ================= |