diff --git a/sledge/src/test/sh_test.ml b/sledge/src/test/sh_test.ml index e9c344192..dfa4f9731 100644 --- a/sledge/src/test/sh_test.ml +++ b/sledge/src/test/sh_test.ml @@ -29,8 +29,7 @@ let%test_module _ = let ( + ) = Term.add let ( - ) = Term.sub let ( = ) = Formula.eq - let f = Term.splat (* any uninterpreted function *) - + let f x = Term.apply (Uninterp "f") [|x|] let wrt = Var.Set.empty let a_, wrt = Var.fresh "a" ~wrt let b_, wrt = Var.fresh "b" ~wrt @@ -156,11 +155,11 @@ let%test_module _ = pp q' ; [%expect {| - ∃ %x_6 . %x_6 = %x_6^ ∧ (-1 + %y_7) = %y_7^ ∧ emp + ∃ %x_6 . %x_6 = f(%x_6) ∧ (-1 + %y_7) = f(%y_7) ∧ emp - ((1 + %y_7^) = %y_7) ∧ emp + ((1 + f(%y_7)) = %y_7) ∧ emp - (-1 + %y_7) = %y_7^ ∧ emp |}] + (-1 + %y_7) = f(%y_7) ∧ emp |}] let%expect_test _ = let q =