Provide more debug information

[CatarinaGamboa]

The previous debug information was not sufficient.
Now we provide more, with the verification conditions used per each variable refinement we got, and with counter example when it fails.

[SMT CHECK]
[SMT] Verifying /Users/cgamboa/git/liquidjava-examples/examples/demo/src/main/java/com/soexamples/study-tasks/typestate-violations/ts-bufferedreader-01/Example.java:28  on 'reader.close();'
[SMT] 
[SMT]   #reader_50 : BufferedReader  true ? state1(#reader_50) == 2 : state1(#reader_50) == 0
[SMT]   #fresh_52 : int              true
[SMT]   ────────────────────────────────────────
[SMT] !state1(#reader_50) == 2
[SMT] result: SAT (subtype fails) — counterexample: state1(#reader_50) = 2

We'be also added coloring and links available.

[Copilot]

Pull request overview

This PR enhances LiquidJava’s debug output during refinement subtyping checks, aiming to make SMT discharge easier to understand by adding structured “[INFO]” and “[SMT]” logs and printing solver outcomes/counterexamples.

Changes:

• Introduces a centralized DebugLog utility to format and gate debug-mode verification logs.
• Extends SMT/subtyping call paths with a silent flag to suppress nested/duplicate debug output where needed.
• Expands ANSI color support in Colors to support the new log formatting.

Reviewed changes

Copilot reviewed 6 out of 6 changed files in this pull request and generated 2 comments.

Show a summary per file

File	Description
liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java	Adds debug logging hooks around SMT discharge and solver outcomes; introduces silent overload.
liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java	Routes subtype checks through a shared discharge helper and adds higher-level debug context logging.
liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java	Threads silent through state SMT checks.
liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java	Uses silent=true for an internal state check to avoid noisy debug output.
liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java	New centralized debug logging implementation for SMT/subtyping verification.
liquidjava-verifier/src/main/java/liquidjava/diagnostics/Colors.java	Adds more ANSI color constants and changes how escape codes are represented.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.