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

fix #2793

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-12-09 07:38:47 +03:00
parent db02328cf3
commit 99a91ee116
1 changed files with 3 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -164,6 +164,9 @@ lbool pb_rewriter_util<PBU>::normalize(typename PBU::args_t& args, typename PBU:
}
}
if (is_eq && k.is_neg()) {
return l_false;
}
if (is_eq) {
TRACE("pb_verbose", display(tout << "post-normalize:", args, k, is_eq););
return l_undef;