mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
duality fixes
This commit is contained in:
parent
2417b75d8d
commit
3e91037a4d
|
@ -1729,6 +1729,8 @@ namespace Duality {
|
|||
class DerivationTree {
|
||||
public:
|
||||
|
||||
virtual ~DerivationTree(){}
|
||||
|
||||
DerivationTree(Duality *_duality, RPFP *rpfp, Reporter *_reporter, Heuristic *_heuristic, bool _full_expand)
|
||||
: slvr(rpfp->slvr()),
|
||||
ctx(rpfp->ctx)
|
||||
|
@ -2207,6 +2209,7 @@ namespace Duality {
|
|||
|
||||
if(ExpandSomeNodes(false,expand_max))
|
||||
continue;
|
||||
tree->Pop(1);
|
||||
while(stack.size() > 1){
|
||||
tree->Pop(1);
|
||||
stack.pop_back();
|
||||
|
|
Loading…
Reference in a new issue