mirror of
https://github.com/Z3Prover/z3
synced 2026-06-06 00:50:54 +00:00
add extra parameter
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
31a85925ee
commit
86dc55691d
2 changed files with 2 additions and 2 deletions
|
|
@ -312,7 +312,7 @@ namespace smt {
|
||||||
* - membership axioms
|
* - membership axioms
|
||||||
* - assume eqs axioms
|
* - assume eqs axioms
|
||||||
*/
|
*/
|
||||||
final_check_status theory_finite_set::final_check_eh() {
|
final_check_status theory_finite_set::final_check_eh(unsigned) {
|
||||||
TRACE(finite_set, tout << "final_check_eh\n";);
|
TRACE(finite_set, tout << "final_check_eh\n";);
|
||||||
|
|
||||||
if (activate_unasserted_clause())
|
if (activate_unasserted_clause())
|
||||||
|
|
|
||||||
|
|
@ -156,7 +156,7 @@ namespace smt {
|
||||||
void new_eq_eh(theory_var v1, theory_var v2) override;
|
void new_eq_eh(theory_var v1, theory_var v2) override;
|
||||||
void new_diseq_eh(theory_var v1, theory_var v2) override;
|
void new_diseq_eh(theory_var v1, theory_var v2) override;
|
||||||
void apply_sort_cnstr(enode *n, sort *s) override;
|
void apply_sort_cnstr(enode *n, sort *s) override;
|
||||||
final_check_status final_check_eh() override;
|
final_check_status final_check_eh(unsigned) override;
|
||||||
bool can_propagate() override;
|
bool can_propagate() override;
|
||||||
void propagate() override;
|
void propagate() override;
|
||||||
void assign_eh(bool_var v, bool is_true) override;
|
void assign_eh(bool_var v, bool is_true) override;
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue