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

fix #3129

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-09 08:13:05 +01:00
parent ee1f7edfa0
commit bbcfd79bf6
1 changed files with 2 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/tactic/ctx_solver_simplify_tactic.cpp
View file

@ -95,6 +95,8 @@ protected:
m_solver.push(); m_solver.push();
reduce(fml); reduce(fml);
m_solver.pop(1); m_solver.pop(1);
if (m.canceled())
return;
SASSERT(m_solver.get_scope_level() == 0); SASSERT(m_solver.get_scope_level() == 0);
TRACE("ctx_solver_simplify_tactic", TRACE("ctx_solver_simplify_tactic",
for (unsigned i = 0; i < fmls.size(); ++i) { for (unsigned i = 0; i < fmls.size(); ++i) {