From d52170271e9c02b677e2f227e4cee5dbd119cb78 Mon Sep 17 00:00:00 2001
From: octalsrc <nicklewchenko92@gmail.com>
Date: Thu, 21 Mar 2024 16:07:25 -0600
Subject: [PATCH 1/3] Add tests for 1-arg through 12-arg uninterpreted
 functions

---
 .../TestSuite/Uninterpreted/Function.hs       | 108 ++++++++++++++++++
 1 file changed, 108 insertions(+)

diff --git a/SBVTestSuite/TestSuite/Uninterpreted/Function.hs b/SBVTestSuite/TestSuite/Uninterpreted/Function.hs
index ac5420a4d..9e37ae382 100644
--- a/SBVTestSuite/TestSuite/Uninterpreted/Function.hs
+++ b/SBVTestSuite/TestSuite/Uninterpreted/Function.hs
@@ -17,8 +17,116 @@ import Documentation.SBV.Examples.Uninterpreted.Function
 
 import Utils.SBVTestFramework
 
+f1 :: SWord8 -> SBool
+f1 = uninterpret "f1"
+
+f2 :: SWord8 -> SWord8 -> SBool
+f2 = uninterpret "f2"
+
+f3 :: SWord8 -> SWord8 -> SWord8 -> SBool
+f3 = uninterpret "f3"
+
+f4 :: SWord8 -> SWord8 -> SWord8 -> SWord8 -> SBool
+f4 = uninterpret "f4"
+
+f5 :: SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SBool
+f5 = uninterpret "f5"
+
+f6 :: SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SBool
+f6 = uninterpret "f6"
+
+f7 :: SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SBool
+f7 = uninterpret "f7"
+
+f8 :: SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SBool
+f8 = uninterpret "f8"
+
+f9 :: SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SBool
+f9 = uninterpret "f9"
+
+f10 :: SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SBool
+f10 = uninterpret "f10"
+
+f11 :: SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SBool
+f11 = uninterpret "f11"
+
+f12 :: SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SBool
+f12 = uninterpret "f12"
+
+thm1 :: SWord8 -> SWord8 -> SBool
+thm1 x a1 =
+  x .== a1
+  .=> f1 x .== f1 a1
+
+thm2 :: SWord8 -> SWord8 -> SWord8 -> SBool
+thm2 x a1 a2 =
+  x .== a1
+  .=> f2 x a2 .== f2 a1 a2
+
+thm3 :: SWord8 -> SWord8 -> SWord8 -> SWord8 -> SBool
+thm3 x a1 a2 a3 =
+  x .== a1
+  .=> f3 x a2 a3 .== f3 a1 a2 a3
+
+thm4 :: SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SBool
+thm4 x a1 a2 a3 a4 =
+  x .== a1
+  .=> f4 x a2 a3 a4 .== f4 a1 a2 a3 a4
+
+thm5 :: SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SBool
+thm5 x a1 a2 a3 a4 a5 =
+  x .== a1
+  .=> f5 x a2 a3 a4 a5 .== f5 a1 a2 a3 a4 a5
+
+thm6 :: SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SBool
+thm6 x a1 a2 a3 a4 a5 a6 =
+  x .== a1
+  .=> f6 x a2 a3 a4 a5 a6 .== f6 a1 a2 a3 a4 a5 a6
+
+thm7 :: SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SBool
+thm7 x a1 a2 a3 a4 a5 a6 a7 =
+  x .== a1
+  .=> f7 x a2 a3 a4 a5 a6 a7 .== f7 a1 a2 a3 a4 a5 a6 a7
+
+thm8 :: SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SBool
+thm8 x a1 a2 a3 a4 a5 a6 a7 a8 =
+  x .== a1
+  .=> f8 x a2 a3 a4 a5 a6 a7 a8 .== f8 a1 a2 a3 a4 a5 a6 a7 a8
+
+thm9 :: SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SBool
+thm9 x a1 a2 a3 a4 a5 a6 a7 a8 a9 =
+  x .== a1
+  .=> f9 x a2 a3 a4 a5 a6 a7 a8 a9 .== f9 a1 a2 a3 a4 a5 a6 a7 a8 a9
+
+thm10 :: SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SBool
+thm10 x a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 =
+  x .== a1
+  .=> f10 x a2 a3 a4 a5 a6 a7 a8 a9 a10 .== f10 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10
+
+thm11 :: SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SBool
+thm11 x a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 =
+  x .== a1
+  .=> f11 x a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 .== f11 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11
+
+thm12 :: SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SBool
+thm12 x a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 =
+  x .== a1
+  .=> f12 x a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 .== f12 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12
+
 tests :: TestTree
 tests =
   testGroup "Uninterpreted.Function"
   [ testCase "aufunc-0" (assertIsThm thmGood)
+  , testCase "aufunc-1" (assertIsThm thm1)
+  , testCase "aufunc-2" (assertIsThm thm2)
+  , testCase "aufunc-3" (assertIsThm thm3)
+  , testCase "aufunc-4" (assertIsThm thm4)
+  , testCase "aufunc-5" (assertIsThm thm5)
+  , testCase "aufunc-6" (assertIsThm thm6)
+  , testCase "aufunc-7" (assertIsThm thm7)
+  , testCase "aufunc-8" (assertIsThm thm8)
+  , testCase "aufunc-9" (assertIsThm thm9)
+  , testCase "aufunc-10" (assertIsThm thm10)
+  , testCase "aufunc-11" (assertIsThm thm11)
+  , testCase "aufunc-12" (assertIsThm thm12)
   ]

From d286c3a261eeeeea951aeaf9b8675e3324e0c78e Mon Sep 17 00:00:00 2001
From: octalsrc <nicklewchenko92@gmail.com>
Date: Fri, 22 Mar 2024 14:37:49 -0600
Subject: [PATCH 2/3] Change Uninterpreted.Function tests to use distinct
 argument sorts

This changes the Uninterpreted.Function tests to use distinct sorts
for every argument, so that any argument mis-orderings in the
SMTDefinable instances will cause tests to fail.
---
 .../TestSuite/Uninterpreted/Function.hs       | 91 ++++++++++++++-----
 1 file changed, 67 insertions(+), 24 deletions(-)

diff --git a/SBVTestSuite/TestSuite/Uninterpreted/Function.hs b/SBVTestSuite/TestSuite/Uninterpreted/Function.hs
index 9e37ae382..ed7c59259 100644
--- a/SBVTestSuite/TestSuite/Uninterpreted/Function.hs
+++ b/SBVTestSuite/TestSuite/Uninterpreted/Function.hs
@@ -9,6 +9,12 @@
 -- Testsuite for Documentation.SBV.Examples.Uninterpreted.Function
 -----------------------------------------------------------------------------
 
+{-# LANGUAGE DeriveAnyClass      #-}
+{-# LANGUAGE DeriveDataTypeable  #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneDeriving  #-}
+{-# LANGUAGE TemplateHaskell     #-}
+
 {-# OPTIONS_GHC -Wall -Werror #-}
 
 module TestSuite.Uninterpreted.Function(tests) where
@@ -17,98 +23,135 @@ import Documentation.SBV.Examples.Uninterpreted.Function
 
 import Utils.SBVTestFramework
 
-f1 :: SWord8 -> SBool
+data A1
+mkUninterpretedSort ''A1
+
+data A2
+mkUninterpretedSort ''A2
+
+data A3
+mkUninterpretedSort ''A3
+
+data A4
+mkUninterpretedSort ''A4
+
+data A5
+mkUninterpretedSort ''A5
+
+data A6
+mkUninterpretedSort ''A6
+
+data A7
+mkUninterpretedSort ''A7
+
+data A8
+mkUninterpretedSort ''A8
+
+data A9
+mkUninterpretedSort ''A9
+
+data A10
+mkUninterpretedSort ''A10
+
+data A11
+mkUninterpretedSort ''A11
+
+data A12
+mkUninterpretedSort ''A12
+
+
+f1 :: SA1 -> SBool
 f1 = uninterpret "f1"
 
-f2 :: SWord8 -> SWord8 -> SBool
+f2 :: SA1 -> SA2 -> SBool
 f2 = uninterpret "f2"
 
-f3 :: SWord8 -> SWord8 -> SWord8 -> SBool
+f3 :: SA1 -> SA2 -> SA3 -> SBool
 f3 = uninterpret "f3"
 
-f4 :: SWord8 -> SWord8 -> SWord8 -> SWord8 -> SBool
+f4 :: SA1 -> SA2 -> SA3 -> SA4 -> SBool
 f4 = uninterpret "f4"
 
-f5 :: SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SBool
+f5 :: SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SBool
 f5 = uninterpret "f5"
 
-f6 :: SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SBool
+f6 :: SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SA6 -> SBool
 f6 = uninterpret "f6"
 
-f7 :: SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SBool
+f7 :: SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SA6 -> SA7 -> SBool
 f7 = uninterpret "f7"
 
-f8 :: SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SBool
+f8 :: SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SA6 -> SA7 -> SA8 -> SBool
 f8 = uninterpret "f8"
 
-f9 :: SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SBool
+f9 :: SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SA6 -> SA7 -> SA8 -> SA9 -> SBool
 f9 = uninterpret "f9"
 
-f10 :: SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SBool
+f10 :: SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SA6 -> SA7 -> SA8 -> SA9 -> SA10 -> SBool
 f10 = uninterpret "f10"
 
-f11 :: SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SBool
+f11 :: SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SA6 -> SA7 -> SA8 -> SA9 -> SA10 -> SA11 -> SBool
 f11 = uninterpret "f11"
 
-f12 :: SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SBool
+f12 :: SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SA6 -> SA7 -> SA8 -> SA9 -> SA10 -> SA11 -> SA12 -> SBool
 f12 = uninterpret "f12"
 
-thm1 :: SWord8 -> SWord8 -> SBool
+thm1 :: SA1 -> SA1 -> SBool
 thm1 x a1 =
   x .== a1
   .=> f1 x .== f1 a1
 
-thm2 :: SWord8 -> SWord8 -> SWord8 -> SBool
+thm2 :: SA1 -> SA1 -> SA2 -> SBool
 thm2 x a1 a2 =
   x .== a1
   .=> f2 x a2 .== f2 a1 a2
 
-thm3 :: SWord8 -> SWord8 -> SWord8 -> SWord8 -> SBool
+thm3 :: SA1 -> SA1 -> SA2 -> SA3 -> SBool
 thm3 x a1 a2 a3 =
   x .== a1
   .=> f3 x a2 a3 .== f3 a1 a2 a3
 
-thm4 :: SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SBool
+thm4 :: SA1 -> SA1 -> SA2 -> SA3 -> SA4 -> SBool
 thm4 x a1 a2 a3 a4 =
   x .== a1
   .=> f4 x a2 a3 a4 .== f4 a1 a2 a3 a4
 
-thm5 :: SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SBool
+thm5 :: SA1 -> SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SBool
 thm5 x a1 a2 a3 a4 a5 =
   x .== a1
   .=> f5 x a2 a3 a4 a5 .== f5 a1 a2 a3 a4 a5
 
-thm6 :: SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SBool
+thm6 :: SA1 -> SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SA6 -> SBool
 thm6 x a1 a2 a3 a4 a5 a6 =
   x .== a1
   .=> f6 x a2 a3 a4 a5 a6 .== f6 a1 a2 a3 a4 a5 a6
 
-thm7 :: SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SBool
+thm7 :: SA1 -> SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SA6 -> SA7 -> SBool
 thm7 x a1 a2 a3 a4 a5 a6 a7 =
   x .== a1
   .=> f7 x a2 a3 a4 a5 a6 a7 .== f7 a1 a2 a3 a4 a5 a6 a7
 
-thm8 :: SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SBool
+thm8 :: SA1 -> SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SA6 -> SA7 -> SA8 -> SBool
 thm8 x a1 a2 a3 a4 a5 a6 a7 a8 =
   x .== a1
   .=> f8 x a2 a3 a4 a5 a6 a7 a8 .== f8 a1 a2 a3 a4 a5 a6 a7 a8
 
-thm9 :: SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SBool
+thm9 :: SA1 -> SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SA6 -> SA7 -> SA8 -> SA9 -> SBool
 thm9 x a1 a2 a3 a4 a5 a6 a7 a8 a9 =
   x .== a1
   .=> f9 x a2 a3 a4 a5 a6 a7 a8 a9 .== f9 a1 a2 a3 a4 a5 a6 a7 a8 a9
 
-thm10 :: SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SBool
+thm10 :: SA1 -> SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SA6 -> SA7 -> SA8 -> SA9 -> SA10 -> SBool
 thm10 x a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 =
   x .== a1
   .=> f10 x a2 a3 a4 a5 a6 a7 a8 a9 a10 .== f10 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10
 
-thm11 :: SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SBool
+thm11 :: SA1 -> SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SA6 -> SA7 -> SA8 -> SA9 -> SA10 -> SA11 -> SBool
 thm11 x a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 =
   x .== a1
   .=> f11 x a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 .== f11 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11
 
-thm12 :: SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SWord8 -> SBool
+thm12 :: SA1 -> SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SA6 -> SA7 -> SA8 -> SA9 -> SA10 -> SA11 -> SA12 -> SBool
 thm12 x a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 =
   x .== a1
   .=> f12 x a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 .== f12 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12

From 89100105fd440cc364af023d724ddfeca1d9fd3c Mon Sep 17 00:00:00 2001
From: octalsrc <nicklewchenko92@gmail.com>
Date: Mon, 18 Mar 2024 13:32:20 -0600
Subject: [PATCH 3/3] Fix SMTDefinable instances for 8-arg through 12-arg ui
 functions

SBVTypes fed to the newUninterpreted function were in the wrong order.
---
 Data/SBV/Core/Model.hs | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/Data/SBV/Core/Model.hs b/Data/SBV/Core/Model.hs
index a16430c0c..13b65bc83 100644
--- a/Data/SBV/Core/Model.hs
+++ b/Data/SBV/Core/Model.hs
@@ -2611,7 +2611,7 @@ instance (SymVal i, SymVal h, SymVal g, SymVal f, SymVal e, SymVal d, SymVal c,
                  result st = do isSMT <- inSMTMode st
                                 case (isSMT, uiKind) of
                                   (True, UICodeC (v, _)) -> sbvToSV st (v arg0 arg1 arg2 arg3 arg4 arg5 arg6 arg7)
-                                  _                      -> do newUninterpreted st (nm, mbArgs) (SBVType [kh, kg, kf, ke, kd, kc, kb, ka, ki]) =<< retrieveUICode nm st ka uiKind
+                                  _                      -> do newUninterpreted st (nm, mbArgs) (SBVType [ki, kh, kg, kf, ke, kd, kc, kb, ka]) =<< retrieveUICode nm st ka uiKind
                                                                sw0 <- sbvToSV st arg0
                                                                sw1 <- sbvToSV st arg1
                                                                sw2 <- sbvToSV st arg2
@@ -2647,7 +2647,7 @@ instance (SymVal j, SymVal i, SymVal h, SymVal g, SymVal f, SymVal e, SymVal d,
                  result st = do isSMT <- inSMTMode st
                                 case (isSMT, uiKind) of
                                   (True, UICodeC (v, _)) -> sbvToSV st (v arg0 arg1 arg2 arg3 arg4 arg5 arg6 arg7 arg8)
-                                  _                      -> do newUninterpreted st (nm, mbArgs) (SBVType [kh, kg, kf, ke, kd, kc, kb, ka, ki, kj]) =<< retrieveUICode nm st ka uiKind
+                                  _                      -> do newUninterpreted st (nm, mbArgs) (SBVType [kj, ki, kh, kg, kf, ke, kd, kc, kb, ka]) =<< retrieveUICode nm st ka uiKind
                                                                sw0 <- sbvToSV st arg0
                                                                sw1 <- sbvToSV st arg1
                                                                sw2 <- sbvToSV st arg2
@@ -2685,7 +2685,7 @@ instance (SymVal k, SymVal j, SymVal i, SymVal h, SymVal g, SymVal f, SymVal e,
                  result st = do isSMT <- inSMTMode st
                                 case (isSMT, uiKind) of
                                   (True, UICodeC (v, _)) -> sbvToSV st (v arg0 arg1 arg2 arg3 arg4 arg5 arg6 arg7 arg8 arg9)
-                                  _                      -> do newUninterpreted st (nm, mbArgs) (SBVType [kh, kg, kf, ke, kd, kc, kb, ka, ki, kj, kk]) =<< retrieveUICode nm st ka uiKind
+                                  _                      -> do newUninterpreted st (nm, mbArgs) (SBVType [kk, kj, ki, kh, kg, kf, ke, kd, kc, kb, ka]) =<< retrieveUICode nm st ka uiKind
                                                                sw0 <- sbvToSV st arg0
                                                                sw1 <- sbvToSV st arg1
                                                                sw2 <- sbvToSV st arg2
@@ -2725,7 +2725,7 @@ instance (SymVal l, SymVal k, SymVal j, SymVal i, SymVal h, SymVal g, SymVal f,
                  result st = do isSMT <- inSMTMode st
                                 case (isSMT, uiKind) of
                                   (True, UICodeC (v, _)) -> sbvToSV st (v arg0 arg1 arg2 arg3 arg4 arg5 arg6 arg7 arg8 arg9 arg10)
-                                  _                      -> do newUninterpreted st (nm, mbArgs) (SBVType [kh, kg, kf, ke, kd, kc, kb, ka, ki, kj, kk, kl]) =<< retrieveUICode nm st ka uiKind
+                                  _                      -> do newUninterpreted st (nm, mbArgs) (SBVType [kl, kk, kj, ki, kh, kg, kf, ke, kd, kc, kb, ka]) =<< retrieveUICode nm st ka uiKind
                                                                sw0  <- sbvToSV st arg0
                                                                sw1  <- sbvToSV st arg1
                                                                sw2  <- sbvToSV st arg2
@@ -2767,7 +2767,7 @@ instance (SymVal m, SymVal l, SymVal k, SymVal j, SymVal i, SymVal h, SymVal g,
                  result st = do isSMT <- inSMTMode st
                                 case (isSMT, uiKind) of
                                   (True, UICodeC (v, _)) -> sbvToSV st (v arg0 arg1 arg2 arg3 arg4 arg5 arg6 arg7 arg8 arg9 arg10 arg11)
-                                  _                      -> do newUninterpreted st (nm, mbArgs) (SBVType [kh, kg, kf, ke, kd, kc, kb, ka, ki, kj, kk, kl, km]) =<< retrieveUICode nm st ka uiKind
+                                  _                      -> do newUninterpreted st (nm, mbArgs) (SBVType [km, kl, kk, kj, ki, kh, kg, kf, ke, kd, kc, kb, ka]) =<< retrieveUICode nm st ka uiKind
                                                                sw0  <- sbvToSV st arg0
                                                                sw1  <- sbvToSV st arg1
                                                                sw2  <- sbvToSV st arg2