Script 'mail_helper' called by obssrc Hello community, here is the log from the commit of package z3 for openSUSE:Factory checked in at 2022-09-13 15:09:43 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Comparing /work/SRC/openSUSE:Factory/z3 (Old) and /work/SRC/openSUSE:Factory/.z3.new.2083 (New) ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Package is "z3" Tue Sep 13 15:09:43 2022 rev:35 rq:1003077 version:4.11.2 Changes: -------- --- /work/SRC/openSUSE:Factory/z3/z3.changes 2022-08-29 09:43:15.547839982 +0200 +++ /work/SRC/openSUSE:Factory/.z3.new.2083/z3.changes 2022-09-13 15:11:11.856948100 +0200 @@ -1,0 +2,25 @@ +Mon Sep 12 19:52:13 UTC 2022 - Dirk M??ller <dmuel...@suse.com> + +- update to 4.11.2: + * add error handling to fromString method in JavaScript + * fix regression in default parameters for CDCL, thanks to Nuno Lopes + * fix model evaluation bugs for as-array nested under functions (data-type constructors) + * add rewrite simplifications for datatypes with a single constructor + * add "Global Guidance" capability to SPACER, thanks to Arie Gurfinkel and Hari Gorvind. + * change proof logging format for the new core to use SMTLIB commands. + The format was so far an extension of DRAT used by SAT solvers, but not well compatible + with SMT format that is extensible. The resulting format is a mild extension of SMTLIB with + three extra commands assume, learn, del. They track input clauses, generated clauses and deleted clauses. + They are optionally augmented by proof hints. Two proof hints are used in the current version: "rup" and "farkas". + "rup" is used whent the generated clause can be justified by reverse unit propagation. "farkas" is used when + the clause can be justified by a combination of Farkas cutting planes. There is a built-in proof checker for the + format. Quantifier instantiations are also tracked as proof hints. + Other proof hints are to be added as the feature set is tested and developed. The fallback, buit-in, + self-checker uses z3 to check that the generated clause is a consequence. Note that this is generally + insufficient as generated clauses are in principle required to only be satisfiability preserving. + Proof checking and tranformation operations is overall open ended. + The log for the first commit introducing this change contains further information on the format. + * fix to re-entrancy bug in user propagator (thanks to Clemens Eisenhofer). + * handle _toExpr for quantified formulas in JS bindings + +------------------------------------------------------------------- Old: ---- z3-4.11.0.tar.gz New: ---- z3-4.11.2.tar.gz ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Other differences: ------------------ ++++++ z3.spec ++++++ --- /var/tmp/diff_new_pack.oxtetq/_old 2022-09-13 15:11:12.292949327 +0200 +++ /var/tmp/diff_new_pack.oxtetq/_new 2022-09-13 15:11:12.292949327 +0200 @@ -18,7 +18,7 @@ %define sover 4_11 Name: z3 -Version: 4.11.0 +Version: 4.11.2 Release: 0 Summary: Theorem prover from Microsoft Research License: MIT ++++++ z3-4.11.0.tar.gz -> z3-4.11.2.tar.gz ++++++ ++++ 15661 lines of diff (skipped)
