mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

improved SLS

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-03-21 14:48:01 -07:00
parent f8348d0bc4
commit 5b1f83a676
1 changed files with 4 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -141,7 +141,8 @@ lbool pb_rewriter_util<PBU>::normalize(typename PBU::args_t& args, typename PBU:
for (unsigned i = 0; i < args.size(); ++i) {
args[i].second = PBU::numeral::one();
}
k = PBU::numeral(args.size());
typename PBU::numeral num(args.size());
k = num;
return l_undef;
}
@ -184,7 +185,8 @@ lbool pb_rewriter_util<PBU>::normalize(typename PBU::args_t& args, typename PBU:
for (unsigned i = 0; i < args.size(); ++i) {
args[i].second = PBU::numeral::one();
}
k = PBU::numeral(args.size());
typename PBU::numeral num(args.size());
k = num;
}
// apply cutting plane reduction: