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

add python file

Browse source 
Signed-off-by: Lev Nachmanson <levnach@Levs-MacBook-Pro.local>
This commit is contained in:
Lev Nachmanson 2025-08-06 16:50:22 -07:00 • committed by Lev Nachmanson
parent 31a30370ac
commit d218e87f76
2 changed files with 37 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/smt/theory_lra.cpp
View file

@ -1017,6 +1017,7 @@ public:
void apply_sort_cnstr(enode* n, sort*) {
TRACE(arith, tout << "sort constraint: " << pp(n) << "\n";);
std::cout << "sort constraint: " << pp(n) << " " << __FILE__ << ":" << __LINE__ << "\n";
#if 0
if (!th.is_attached_to_var(n))
mk_var(n->get_owner());