mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 11:42:28 +00:00
Code Activity

following the review comments

Browse source
This commit is contained in:
Lev Nachmanson 2025-06-27 19:48:51 -07:00
parent 84a6e4d672
commit 28d0b471ff
2 changed files with 2 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/math/lp/nla_order_lemmas.cpp
View file

@ -10,7 +10,6 @@
#include "math/lp/nla_core.h"
#include "math/lp/nla_common.h"
#include "math/lp/factorization_factory_imp.h"
#include "util/trail.h"
namespace nla {

4
src/math/lp/nla_types.h
View file

@ -66,8 +66,8 @@ namespace nla {
class core;
//
// lemmas are created in a scope.
// when the destructor of new_lemma is invoked
// all constraints are assumed added to the lemma
// when the destructor of lemma_builder is invoked
// all constraints are assumed already added to the current_lemma
// correctness of the lemma can be checked at this point.
//
class lemma_builder {