cvc5-1.1.2

New Features

• Added support for nullable sorts and lift operator to the theory of datatypes.
• Adds a new strategy --sub-cbqi (disabled by default) for quantifier
  instantiation which uses subsolvers to compute unsat cores of instantiations
  that are used in proofs of unsatisfiability.

Changes

• SAT clauses are no longer marked as removable in MiniSat. This change
  improves performance overall on quantifier-free logics with arithmetic and
  strings.
• API
  • Functions kindToString(Kind) and sortKindToString(SortKind) are now
    deprecated and replaced by std::to_string(Kind) and
    std::to_string(SortKind). They will be removed in the next minor release.
• Minor changes to the output format for proofs. Proofs in the AletheLF
  proof format generated by cvc5 now correspond directly to their representation
  in proof objects obtained in via the API (the Proof class). Moreover,
  proofs now use SMT-LIB compliant syntax for quantified formulas and unary
  arithmetic negation.
• The option --safe-options now disallows cases where more than one regular
  option is used.
• Fixes the parsing of define-fun-rec and define-funs-rec in interactive
  mode.
• Renamed bag.duplicate_removal to bag.setof.
• Improvements to handling of constant production rules (Constant) in SyGuS
  grammars.