mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

remove experiment with theory lemmas

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-10-29 18:48:48 -07:00
parent 3726960969
commit a957a5673d
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/smt/theory_lra.cpp
View file

@ -589,7 +589,7 @@ class theory_lra::imp {
void mk_clause(literal l1, literal l2, unsigned num_params, parameter * params) { void mk_clause(literal l1, literal l2, unsigned num_params, parameter * params) {
TRACE("arith", literal lits[2]; lits[0] = l1; lits[1] = l2; ctx().display_literals_verbose(tout, 2, lits); tout << "\n";); TRACE("arith", literal lits[2]; lits[0] = l1; lits[1] = l2; ctx().display_literals_verbose(tout, 2, lits); tout << "\n";);
ctx().mk_th_lemma(get_id(), l1, l2, num_params, params); ctx().mk_th_axiom(get_id(), l1, l2, num_params, params);
} }
void mk_clause(literal l1, literal l2, literal l3, unsigned num_params, parameter * params) { void mk_clause(literal l1, literal l2, literal l3, unsigned num_params, parameter * params) {
@ -3342,7 +3342,7 @@ public:
// The lemmas can come in batches // The lemmas can come in batches
// and the same literal can appear in several lemmas in a batch: it becomes l_true // and the same literal can appear in several lemmas in a batch: it becomes l_true
// in earlier processing, but it was not so when the lemma was produced // in earlier processing, but it was not so when the lemma was produced
ctx().mk_th_lemma(get_id(), m_core.size(), m_core.data()); ctx().mk_th_axiom(get_id(), m_core.size(), m_core.data());
} }
} }