mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
force propagation for smt cubing
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
bbfac99b22
commit
e950453685
|
@ -281,6 +281,9 @@ namespace smt {
|
|||
ast_manager& m = get_manager();
|
||||
if (!m_cuber) {
|
||||
m_cuber = alloc(cuber, *this);
|
||||
// force propagation
|
||||
push_core();
|
||||
pop_core(1);
|
||||
}
|
||||
expr_ref result = m_cuber->cube();
|
||||
expr_ref_vector lits(m);
|
||||
|
|
|
@ -264,7 +264,8 @@ public:
|
|||
}
|
||||
|
||||
expr_ref_vector cube(expr_ref_vector& vars, unsigned backtrack_level) override {
|
||||
return m_solver1->cube(vars, backtrack_level);
|
||||
switch_inc_mode();
|
||||
return m_solver2->cube(vars, backtrack_level);
|
||||
}
|
||||
|
||||
expr * get_assumption(unsigned idx) const override {
|
||||
|
|
|
@ -80,6 +80,7 @@ public:
|
|||
|
||||
expr_ref_vector cube(expr_ref_vector& vars, unsigned ) override {
|
||||
set_reason_unknown("cubing is not supported on tactics");
|
||||
IF_VERBOSE(1, verbose_stream() << "cubing is not supported on tactics\n");
|
||||
return expr_ref_vector(get_manager());
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue