mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 02:42:02 +00:00
Code Activity

Fix add external lemmas to solver even if use_bg_invs=false

Browse source 
spacer.use_bg_invs controls how user-supplied invariants are used.
However, the user expects them to be used independent of the option.
This commit is contained in:
Arie Gurfinkel 2018-09-05 10:36:25 -04:00
parent a000747605
commit 58d93d8907
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/muz/spacer/spacer_context.cpp
View file

@ -2507,7 +2507,7 @@ void context::add_cover(int level, func_decl* p, expr* property, bool bg)
} }
void context::add_invariant (func_decl *p, expr *property) void context::add_invariant (func_decl *p, expr *property)
{add_cover (infty_level(), p, property, true);} {add_cover (infty_level(), p, property, use_bg_invs());}
expr_ref context::get_reachable(func_decl *p) { expr_ref context::get_reachable(func_decl *p) {
pred_transformer* pt = nullptr; pred_transformer* pt = nullptr;