diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2020-06-05 11:10:34 -0300 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-06-05 11:10:34 -0300 |
| commit | 7aa98fa461932db12c05820e685772d2aa983993 (patch) | |
| tree | bf015b4e77c6d2834bf5679d2bd596274c4c749a /NEWS | |
| parent | 80b0795702e71d54ed7c17ba809eebde628eb516 (diff) | |
Changing default language (#4561)
Useful to avoid issues when a language is not set and it cannot be easily inferred (for example via the API). Since the language that covers most operators in CVC4 is the SMT one we use that as default now.
Diffstat (limited to 'NEWS')
| -rw-r--r-- | NEWS | 3 |
1 files changed, 3 insertions, 0 deletions
@@ -9,6 +9,9 @@ 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`. +* The default output language is changed from CVC to SMT-LIB 2.6. The + default output language is used when the problem language cannot be + easily inferred (for example when CVC4 is used from the API). * 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 |