# Changelog veriT follows Calendar Versioning. Version numbers are of the form YYYY.0M.MICRO i.e. year, zero-padded month, and patch level. Compatibility is only assured between versions with the same year and month. The performance on individual benchmarks might even fluctuate between patch levels. ## [2024.12] - 2024-12-31 ### Additions - Add commandline option `--print-cvc5-numbers` that introducts veriT to use cvc5 notation to print literals for rational and integers. Using this option, the literal `(/ (- 3) 5)` will be printed as `-3/5`. Negative numbers are printed without unary minus: -3 instead of (- 3). - Add possibility to print proofs with debug annotations. This must be enabled during compile time using the configuration switch `--enable-proof-debug-annotations`. For some rules, the proof then contains the source code location that introduced a step. Furthermore, `forall_inst` steps are annotated by with the instantiation strategy that generated the instance. ### Changes - veriT now always returns with an error code 14 in case of a timeout and 24 in case of a CPU timeout (when available). This is independent of the operating system. - The error message printed when trying to enable certain options (such as produce-proofs) after issuing `set-logic` is now clearer. ### Incompatible Proof Changes - The printing of sorts in the contexts was extended. Sorts are fixed printed for fixed variable, and for proper substitutions. For example, instead of `(anchor :step t3 :args ((x S) (:= y x)))`, now `(anchor :step t3 :args ((x S) (:= (y S) x)))` is printed. While the sort of `y` could be inferred before, printing it simplifies reconstruction. - The syntax for the arguments of `forall_inst` is changed in accordance with changes to the Alethe standard. Previously it would list assignments to variables in the form `((:= xi T1) .. (:= xn Tn))`. Now it just lists the terms `(Ti .. Tn)`. The order is determined by the order of the variables in the quantifier. - The `la_generic` step now always uses decimal numbers, even if the active logic does not contain the Real sort. Previously, the coefficient 0.5 was printed as `(div 1 2)` if the logic was, for example, `QF_LIA`. Now this would be printed as `(/ 1 2)`. This also affects rationals with a denominator of `1`. Those are guaranteed to be printed using decimals (e.g., `2.0` instead of `2`). - Note that the bugfix on the printing of rational literals described below may affect proof consumers. ### Proof Changes - veriT now never emits the proof rule `implies_simplify` to perform the simplification `(P -> Q) -> Q => P or Q`. Instead, it always emits a `bool_simplify` step. - `bind` steps that do not rename the variables now have a context that is exactly as specified in the Alethe specification. For example, if the conclusion of `bind` is `= (forall ((x S)) (P x)) (forall ((x S)) (Q x))` the context is no `((x S) (:= x x))` while it was just `((x S))` before. ### Bugfixes - Fix a portability issue by ensuring that our own sorting implementation is used everywhere. Otherwise, the behaviour of veriT could depend on how equal values are ordered during sorting. - Fix compilation of the tarball after invoking `make clean`. During cleanup some generated files (such as the lexer) are deleted. We now ship the source file for those generated files to allow recompilation. - The printing of rational literals is SMT-LIB compliant. Previously, the literal `(/ 1 2)` would be printed as `(/ 1.0 2.0)`. The SMT-LIB standard specifies that the syntax for decimal literals is `(/ )` and `(/ (- ) )`. - Sometimes veriT would use the `minus_simplify` rule where the `unary_minus_simplify` rule should have been used. - Fix a bug in the quantifier preprocessor that resulted in an error under some conditions when removing unused variables. ## [2021.06] - 2021-06-29 This release corresponds mostly to veriT as submitted to SMT-COMP 2021. The timeout support for Windows and the proof format change were done after the submission, but they should not affect solving performance. ### Proof Incompatibilities - The contexts provided in anchors are now sorted. Every fixed variable is printed with its sort. The sort of proper substitution in the context can be inferred from the right hand side. The syntax corresponds to the SMT-LIB syntax used in variable lists, such as for `forall`. For example, instead of `(anchor :step t3 :args (x) (:= y x)))`, now `(anchor :step t3 :args ((x S) (:= y x)))` is printed. The sort of `y` is equivalent to the sort of `x`. ### Additions - New preprocessing method: quantifier simplification by unification. It can be deactivated with `--disable-qsimp` and fine tuned with: `--qsimp-delete`, `--qsimp-eager`, `--qsimp-solitary`. For now, this method is not proof producing. - Support `define-fun` when not in proof production mode. - Support setting a wallclock time limit on Windows using `--max-time`. Uses Timer Queues and forces a hard exit. Hence, e.g, statistics will not be printed. - Support setting a CPU time limit on systems with `setitimer` via `--max-virtual-time`. - Recognize QF_LIRA. ### Bugfixes - Fix compilation with -fno-common, the default in gcc10. ## [2020.10] - 2020-10-14 This release is motivated by the inclusion of veriT as a backend for proof reconstruction in Isabelle. It is the first release since 2016. Since the last stable release of veriT, the solver has seen many changes. The changes mainly affect quantifier instantiation and proof production.