From dcde8de10ddefb6e20059e61ef48af4075a12e88 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Fri, 15 Apr 2016 13:30:20 +0200 Subject: [PATCH] [bugfix/medium] Fixed printing of the new reasons --- solver/solver_types.ml | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/solver/solver_types.ml b/solver/solver_types.ml index 9f219c8a..084e0495 100644 --- a/solver/solver_types.ml +++ b/solver/solver_types.ml @@ -257,12 +257,11 @@ module McMake (E : Expr_intf.S) = struct let level a = match a.var.v_level, a.var.reason with - | n, _ when n < 0 -> assert false - | 0, Some (Bcp c) -> sprintf "->0/%s" c.name - | 0, None -> "@0" - | n, Some (Bcp c) -> sprintf "->%d/%s" n c.name - | n, None -> sprintf "@@%d" n - | n, Some (Semantic lvl) -> sprintf "::%d/%d" n lvl + | n, _ when n < 0 -> sprintf "%%" + | n, None -> sprintf "%d" n + | n, Some Decision -> sprintf "@@%d" n + | n, Some Bcp c -> sprintf "->%d/%s" n c.name + | n, Some Semantic lvl -> sprintf "::%d/%d" n lvl let value a = if a.is_true then sprintf "[T%s]" (level a)