From 58d93d8907da066eefc6ff0fbd282c8de7594149 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Wed, 5 Sep 2018 10:36:25 -0400 Subject: [PATCH] Fix add external lemmas to solver even if use_bg_invs=false spacer.use_bg_invs controls how user-supplied invariants are used. However, the user expects them to be used independent of the option. --- src/muz/spacer/spacer_context.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index 308b07d1a..fd16e99f6 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -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) -{add_cover (infty_level(), p, property, true);} +{add_cover (infty_level(), p, property, use_bg_invs());} expr_ref context::get_reachable(func_decl *p) { pred_transformer* pt = nullptr;