[sledge] Use an actual uninterpreted function in Sh tests

Reviewed By: jvillard

Differential Revision: D24920762

fbshipit-source-id: 51a015dd7

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 =