mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 18:05:21 +00:00
Code Activity

fix #5882. Use model true when inlining (#5892)

Browse source
This commit is contained in:
Hari Govind V K 2022-03-09 15:31:39 -05:00 committed by GitHub
parent 8e18a94558
commit f26c12a9ad
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/muz/transforms/dl_mk_rule_inliner.cpp
View file

@ -449,7 +449,7 @@ namespace datalog {
}
}
if (modified) {
datalog::del_rule(m_mc, *r0, l_false);
datalog::del_rule(m_mc, *r0, l_true);
}
return modified;