mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity

fix #3774

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-05 13:59:28 -07:00
parent 550852bc62
commit bb1119a6ca
1 changed files with 5 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/muz/base/hnf.cpp
View file

@ -244,7 +244,12 @@ private:
premise = mk_modus_ponens(premise, p1); premise = mk_modus_ponens(premise, p1);
fml = fml1; fml = fml1;
} }
else if (fml1 != fml) {
premise = mk_modus_ponens(premise, m.mk_rewrite(fml, fml1));
fml = fml1;
} }
}
SASSERT(!premise || (fml1 == fml && fml == m.get_fact(premise)));
head = fml0; head = fml0;
while (m.is_implies(head, e1, e2)) { while (m.is_implies(head, e1, e2)) {
m_body.push_back(e1); m_body.push_back(e1);