mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

update smt logging format to follow SAT solver

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-08-20 19:56:44 -07:00
parent 77088745d0
commit ecb43ccca2
6 changed files with 95 additions and 24 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/rewriter/pb_rewriter_def.h
View file

@ -258,9 +258,7 @@ lbool pb_rewriter_util<PBU>::normalize(typename PBU::args_t& args, typename PBU:
typename PBU::numeral n0 = k/max;
typename PBU::numeral n1 = floor(n0);
typename PBU::numeral n2 = ceil(k/min) - PBU::numeral::one();
if (n1 == n2 && !n0.is_int()) {
IF_VERBOSE(3, display(verbose_stream() << "set cardinality\n", args, k, is_eq););
if (n1 == n2 && !n0.is_int()) {
for (unsigned i = 0; i < args.size(); ++i) {
args[i].second = PBU::numeral::one();
}