more info to debug prints

Kirill Golubev · Kirill Golubev · commit cf9735b1ef89 · 2022-10-10T06:09:51.000+03:00
diff --git a/liquidjava/liquidjava-umbrella/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java b/liquidjava/liquidjava-umbrella/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java
@@ -102,7 +102,7 @@ public boolean canProcessSubtyping(Predicate type, Predicate expectedType, List<
             // printError(premises, expectedType, element, map, e.getMessage());
         }
 
-        System.out.println(premises.toString() + "\n" + et.toString());
+        System.out.println("premise: " + premises.toString() + "\nexpectation: " + et.toString());
         return smtChecks(premises, et, element);
     }
 
diff --git a/liquidjava/liquidjava-umbrella/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java b/liquidjava/liquidjava-umbrella/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java
@@ -17,7 +17,7 @@ public void verifySubtype(Predicate subRef, Predicate supRef, Context c)
         // Discharges the verification to z3
 
         Predicate toVerify = Predicate.createConjunction(subRef, supRef.negate());
-        System.out.println(toVerify.toString()); // TODO remove
+        System.out.println("verification query: " + toVerify); // TODO remove
 
         try {
             Expression exp = toVerify.getExpression();

Original file line number	Diff line number	Diff line change
`@@ -102,7 +102,7 @@ public boolean canProcessSubtyping(Predicate type, Predicate expectedType, List<`
`102`	`102`	`// printError(premises, expectedType, element, map, e.getMessage());`
`103`	`103`	`}`
`104`	`104`
`105`		`- System.out.println(premises.toString() + "\n" + et.toString());`
	`105`	`+ System.out.println("premise: " + premises.toString() + "\nexpectation: " + et.toString());`
`106`	`106`	`return smtChecks(premises, et, element);`
`107`	`107`	`}`
`108`	`108`