Fix a chc model parsing bug and change the printing style of refineme…

…nt types
moratorium08 · Sep 21, 2023 · 340e556 · 340e556
1 parent a4b6195
commit 340e556
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/lib/typing/chc_solver.ml b/lib/typing/chc_solver.ml
@@ -238,8 +238,8 @@ let parse_model model =
       | _ -> failwith "program error"
     in
     let rec simplify_def x = match x with
-      | RAnd(x, y) -> RAnd(simplify x, simplify y)
-      | ROr(x, y) -> ROr(simplify x, simplify y)
+      | RAnd(x, y) -> RAnd(simplify_def x, simplify_def y)
+      | ROr(x, y) -> ROr(simplify_def x, simplify_def y)
       | RTemplate((name, args)) -> 
         let (_, vars, form) = List.find_exn defs ~f:(fun (name', _, _) -> (Rid.eq name name')) in
         subst_arg vars args form

diff --git a/lib/typing/rtype.ml b/lib/typing/rtype.ml
@@ -100,7 +100,7 @@ let rec print_rtype = function
     Printf.printf " -> ";
     print_rtype y;
     print_string ")";
-  | RInt x -> Printf.printf "int("; print_rint x; Printf.printf ")"
+  | RInt x -> print_rint x; Printf.printf ": int"
 
 
 let rint2arith = function