mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 13:58:45 +00:00
Code Activity

added rule names to duality output

Browse source
This commit is contained in:
Ken McMillan 2013-05-09 13:31:17 -07:00
parent b935e1e71a
commit dc793907a5
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/muz_qe/duality_dl_interface.cpp
View file

@ -240,6 +240,10 @@ static void print_proof(dl_interface *d, std::ostream& out, Solver::Counterexamp
out << " " << cex.tree->Eval(&edge,edge.F.IndParams[i]);
out << ")\n";
// print the rule number
out << " rule!" << node.Outgoing->map->number;
// print the substitution
out << " (subst\n";