From 1d974c058760f60049e21afcb31f2eed2a0dfd29 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Thu, 12 Nov 2020 16:39:02 -0800
Subject: [PATCH] [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 | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

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 =