mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-21 21:33:39 +00:00
Code Activity

fix #3648

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-01 03:49:48 -07:00
parent cc394f0fe9
commit f98e6a62fe
1 changed files with 1 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/smt/tactic/smt_tactic.cpp
View file

@ -269,6 +269,7 @@ public:
if (pr) { if (pr) {
in->reset(); in->reset();
in->assert_expr(m.get_fact(pr), pr, nullptr); in->assert_expr(m.get_fact(pr), pr, nullptr);
in->updt_prec(goal::UNDER_OVER);
} }
if (m_candidate_models) { if (m_candidate_models) {
switch (m_ctx->last_failure()) { switch (m_ctx->last_failure()) {