make sure registration variables are internal

also update golds
LeventErkok · Dec 27, 2024 · 5e8691a · 5e8691a
1 parent 7f3a3ff
commit 5e8691a
Show file tree

Hide file tree

Showing 10 changed files with 169 additions and 153 deletions.
diff --git a/Data/SBV/Core/Model.hs b/Data/SBV/Core/Model.hs
@@ -59,7 +59,7 @@ module Data.SBV.Core.Model (
 
 import Control.Applicative    (ZipList(ZipList))
 import Control.Monad          (when, unless, mplus)
-import Control.Monad.IO.Class (MonadIO)
+import Control.Monad.IO.Class (MonadIO, liftIO)
 
 import GHC.Generics (M1(..), U1(..), (:*:)(..), K1(..))
 import qualified GHC.Generics as G
@@ -2492,8 +2492,12 @@ class SMTDefinable a where
   cgUninterpret       nm code v = sbvDefineValue nm Nothing   $ UICodeC (v, code)
   sym                           = uninterpret
 
-  default registerSMTFunction :: (a ~ (SBV b -> c), SymVal b, SMTDefinable c) => a -> Symbolic ()
-  registerSMTFunction f = free_ >>= registerSMTFunction . f
+  default registerSMTFunction :: forall b c. (a ~ (SBV b -> c), SymVal b, SMTDefinable c) => a -> Symbolic ()
+  registerSMTFunction f = do let k = kindOf (Proxy @b)
+                             st <- symbolicEnv
+                             v <- liftIO $ internalVariable st k
+                             let b = SBV $ SVal k $ Right $ cache (const (pure v))
+                             registerSMTFunction $ f b
 
 -- | Kind of uninterpretation
 data UIKind a = UIFree  Bool                            -- ^ completely uninterpreted. If Bool is true, then this is curried.

diff --git a/SBVTestSuite/GoldFiles/query_uisatex1.gold b/SBVTestSuite/GoldFiles/query_uisatex1.gold
@@ -20,33 +20,34 @@
 [GOOD] (define-fun s9 () Int (- 3))
 [GOOD] (define-fun s11 () Int 9)
 [GOOD] (define-fun s14 () Int 1)
-[GOOD] (define-fun s17 () Int 0)
-[GOOD] (define-fun s20 () Int 5)
-[GOOD] (define-fun s22 () Int 7)
-[GOOD] (define-fun s24 () Int 6)
-[GOOD] (define-fun s28 () (_ FloatingPoint  8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 4508877.0 524288.0)))
-[GOOD] (define-fun s31 () (_ FloatingPoint  8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 5033165.0 524288.0)))
-[GOOD] (define-fun s32 () Int 121)
-[GOOD] (define-fun s37 () Int 8)
-[GOOD] (define-fun s39 () (_ FloatingPoint  8 24) (_ +oo 8 24))
-[GOOD] (define-fun s41 () String (_ char #x63))
-[GOOD] (define-fun s42 () String "hey")
-[GOOD] (define-fun s44 () (_ FloatingPoint  8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 78.0 1.0)))
-[GOOD] (define-fun s46 () String "tey")
-[GOOD] (define-fun s48 () (_ FloatingPoint  8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 92.0 1.0)))
-[GOOD] (define-fun s50 () String (_ char #x72))
-[GOOD] (define-fun s51 () String "foo")
-[GOOD] (define-fun s53 () (_ FloatingPoint  8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 7.0 2.0)))
-[GOOD] (define-fun s55 () (Seq Int) (seq.++ (seq.unit 1) (seq.unit 2) (seq.unit 3)))
-[GOOD] (define-fun s56 () (Seq (_ FloatingPoint  8 24)) (seq.++ (seq.unit ((_ to_fp 8 24) roundNearestTiesToEven (/ 8598323.0 1048576.0))) (seq.unit ((_ to_fp 8 24) roundNearestTiesToEven (/ 3.0 1.0)))))
-[GOOD] (define-fun s59 () (Seq Int) (seq.++ (seq.unit 9) (seq.unit 5)))
-[GOOD] (define-fun s60 () (Seq (_ FloatingPoint  8 24)) (seq.++ (seq.unit ((_ to_fp 8 24) roundNearestTiesToEven (/ 8598323.0 1048576.0))) (seq.unit ((_ to_fp 8 24) roundNearestTiesToEven (/ 9.0 1.0)))))
-[GOOD] (define-fun s62 () Int 21)
-[GOOD] (define-fun s64 () (Seq Int) (seq.unit 5))
-[GOOD] (define-fun s65 () (Seq (_ FloatingPoint  8 24)) (seq.++ (seq.unit ((_ to_fp 8 24) roundNearestTiesToEven (/ 8598323.0 1048576.0))) (seq.unit (_ +zero 8 24))))
-[GOOD] (define-fun s67 () Int 210)
+[GOOD] (define-fun s21 () Int 5)
+[GOOD] (define-fun s23 () Int 7)
+[GOOD] (define-fun s25 () Int 6)
+[GOOD] (define-fun s29 () (_ FloatingPoint  8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 4508877.0 524288.0)))
+[GOOD] (define-fun s32 () (_ FloatingPoint  8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 5033165.0 524288.0)))
+[GOOD] (define-fun s33 () Int 121)
+[GOOD] (define-fun s38 () Int 8)
+[GOOD] (define-fun s40 () (_ FloatingPoint  8 24) (_ +oo 8 24))
+[GOOD] (define-fun s42 () String (_ char #x63))
+[GOOD] (define-fun s43 () String "hey")
+[GOOD] (define-fun s45 () (_ FloatingPoint  8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 78.0 1.0)))
+[GOOD] (define-fun s47 () String "tey")
+[GOOD] (define-fun s49 () (_ FloatingPoint  8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 92.0 1.0)))
+[GOOD] (define-fun s51 () String (_ char #x72))
+[GOOD] (define-fun s52 () String "foo")
+[GOOD] (define-fun s54 () (_ FloatingPoint  8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 7.0 2.0)))
+[GOOD] (define-fun s56 () (Seq Int) (seq.++ (seq.unit 1) (seq.unit 2) (seq.unit 3)))
+[GOOD] (define-fun s57 () (Seq (_ FloatingPoint  8 24)) (seq.++ (seq.unit ((_ to_fp 8 24) roundNearestTiesToEven (/ 8598323.0 1048576.0))) (seq.unit ((_ to_fp 8 24) roundNearestTiesToEven (/ 3.0 1.0)))))
+[GOOD] (define-fun s60 () (Seq Int) (seq.++ (seq.unit 9) (seq.unit 5)))
+[GOOD] (define-fun s61 () (Seq (_ FloatingPoint  8 24)) (seq.++ (seq.unit ((_ to_fp 8 24) roundNearestTiesToEven (/ 8598323.0 1048576.0))) (seq.unit ((_ to_fp 8 24) roundNearestTiesToEven (/ 9.0 1.0)))))
+[GOOD] (define-fun s63 () Int 21)
+[GOOD] (define-fun s65 () (Seq Int) (seq.unit 5))
+[GOOD] (define-fun s66 () (Seq (_ FloatingPoint  8 24)) (seq.++ (seq.unit ((_ to_fp 8 24) roundNearestTiesToEven (/ 8598323.0 1048576.0))) (seq.unit (_ +zero 8 24))))
+[GOOD] (define-fun s68 () Int 210)
 [GOOD] ; --- top level inputs ---
 [GOOD] (declare-fun s0 () Int)
+[GOOD] (declare-fun s17 () Bool) ; tracks user variable "__internal_sbv_s17"
+[GOOD] (declare-fun s18 () Int) ; tracks user variable "__internal_sbv_s18"
 [GOOD] ; --- constant tables ---
 [GOOD] ; --- non-constant tables ---
 [GOOD] ; --- uninterpreted constants ---
@@ -66,55 +67,59 @@
 [GOOD] (define-fun s13 () Int (q1 s0))
 [GOOD] (define-fun s15 () Int (+ s0 s14))
 [GOOD] (define-fun s16 () Bool (= s13 s15))
-[GOOD] (define-fun s18 () Int (q2 false s17))
-[GOOD] (define-fun s19 () Int (q2 true s5))
-[GOOD] (define-fun s21 () Bool (= s19 s20))
-[GOOD] (define-fun s23 () Int (q2 false s22))
-[GOOD] (define-fun s25 () Bool (= s23 s24))
-[GOOD] (define-fun s26 () Int (q2 false s3))
-[GOOD] (define-fun s27 () Bool (= s5 s26))
-[GOOD] (define-fun s29 () (_ FloatingPoint  8 24) (q3 s28 true s3))
-[GOOD] (define-fun s30 () Bool (fp.eq s28 s29))
-[GOOD] (define-fun s33 () (_ FloatingPoint  8 24) (q3 s31 true s32))
-[GOOD] (define-fun s34 () Bool (fp.isZero s33))
-[GOOD] (define-fun s35 () Bool (fp.isNegative s33))
-[GOOD] (define-fun s36 () Bool (and s34 s35))
-[GOOD] (define-fun s38 () (_ FloatingPoint  8 24) (q3 s31 false s37))
-[GOOD] (define-fun s40 () Bool (fp.eq s38 s39))
-[GOOD] (define-fun s43 () (_ FloatingPoint  8 24) (q4 s41 s42))
-[GOOD] (define-fun s45 () Bool (fp.eq s43 s44))
-[GOOD] (define-fun s47 () (_ FloatingPoint  8 24) (q4 s41 s46))
-[GOOD] (define-fun s49 () Bool (fp.eq s47 s48))
-[GOOD] (define-fun s52 () (_ FloatingPoint  8 24) (q4 s50 s51))
-[GOOD] (define-fun s54 () Bool (fp.eq s52 s53))
-[GOOD] (define-fun s57 () Int (q5 s55 s56))
-[GOOD] (define-fun s58 () Bool (= s22 s57))
-[GOOD] (define-fun s61 () Int (q5 s59 s60))
-[GOOD] (define-fun s63 () Bool (= s61 s62))
-[GOOD] (define-fun s66 () Int (q5 s64 s65))
-[GOOD] (define-fun s68 () Bool (= s66 s67))
+[GOOD] (define-fun s19 () Int (q2 s17 s18))
+[GOOD] (define-fun s20 () Int (q2 true s5))
+[GOOD] (define-fun s22 () Bool (= s20 s21))
+[GOOD] (define-fun s24 () Int (q2 false s23))
+[GOOD] (define-fun s26 () Bool (= s24 s25))
+[GOOD] (define-fun s27 () Int (q2 false s3))
+[GOOD] (define-fun s28 () Bool (= s5 s27))
+[GOOD] (define-fun s30 () (_ FloatingPoint  8 24) (q3 s29 true s3))
+[GOOD] (define-fun s31 () Bool (fp.eq s29 s30))
+[GOOD] (define-fun s34 () (_ FloatingPoint  8 24) (q3 s32 true s33))
+[GOOD] (define-fun s35 () Bool (fp.isZero s34))
+[GOOD] (define-fun s36 () Bool (fp.isNegative s34))
+[GOOD] (define-fun s37 () Bool (and s35 s36))
+[GOOD] (define-fun s39 () (_ FloatingPoint  8 24) (q3 s32 false s38))
+[GOOD] (define-fun s41 () Bool (fp.eq s39 s40))
+[GOOD] (define-fun s44 () (_ FloatingPoint  8 24) (q4 s42 s43))
+[GOOD] (define-fun s46 () Bool (fp.eq s44 s45))
+[GOOD] (define-fun s48 () (_ FloatingPoint  8 24) (q4 s42 s47))
+[GOOD] (define-fun s50 () Bool (fp.eq s48 s49))
+[GOOD] (define-fun s53 () (_ FloatingPoint  8 24) (q4 s51 s52))
+[GOOD] (define-fun s55 () Bool (fp.eq s53 s54))
+[GOOD] (define-fun s58 () Int (q5 s56 s57))
+[GOOD] (define-fun s59 () Bool (= s23 s58))
+[GOOD] (define-fun s62 () Int (q5 s60 s61))
+[GOOD] (define-fun s64 () Bool (= s62 s63))
+[GOOD] (define-fun s67 () Int (q5 s65 s66))
+[GOOD] (define-fun s69 () Bool (= s67 s68))
 [GOOD] ; --- delayedEqualities ---
 [GOOD] ; --- formula ---
 [GOOD] (assert s4)
 [GOOD] (assert s8)
 [GOOD] (assert s12)
 [GOOD] (assert s16)
-[GOOD] (assert s21)
-[GOOD] (assert s25)
-[GOOD] (assert s27)
-[GOOD] (assert s30)
-[GOOD] (assert s36)
-[GOOD] (assert s40)
-[GOOD] (assert s45)
-[GOOD] (assert s49)
-[GOOD] (assert s54)
-[GOOD] (assert s58)
-[GOOD] (assert s63)
-[GOOD] (assert s68)
+[GOOD] (assert s22)
+[GOOD] (assert s26)
+[GOOD] (assert s28)
+[GOOD] (assert s31)
+[GOOD] (assert s37)
+[GOOD] (assert s41)
+[GOOD] (assert s46)
+[GOOD] (assert s50)
+[GOOD] (assert s55)
+[GOOD] (assert s59)
+[GOOD] (assert s64)
+[GOOD] (assert s69)
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (s0))
 [RECV] ((s0 0))
+[SEND] (get-value (s17))
+[RECV] ((s17 false))
+[SEND] (get-value (s18))
+[RECV] ((s18 0))
 [GOOD] (set-option :pp.max_depth      4294967295)
 [GOOD] (set-option :pp.min_alias_size 4294967295)
 [GOOD] (set-option :model.inline_def  true      )

diff --git a/SBVTestSuite/GoldFiles/query_uisatex2.gold b/SBVTestSuite/GoldFiles/query_uisatex2.gold
@@ -20,33 +20,35 @@
 [GOOD] (define-fun s9 () Int (- 3))
 [GOOD] (define-fun s11 () Int 9)
 [GOOD] (define-fun s14 () Int 1)
-[GOOD] (define-fun s17 () Int 0)
-[GOOD] (define-fun s20 () Int 5)
-[GOOD] (define-fun s22 () Int 7)
-[GOOD] (define-fun s24 () Int 6)
-[GOOD] (define-fun s28 () (_ FloatingPoint  8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 4508877.0 524288.0)))
-[GOOD] (define-fun s31 () (_ FloatingPoint  8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 5033165.0 524288.0)))
-[GOOD] (define-fun s32 () Int 121)
-[GOOD] (define-fun s37 () Int 8)
-[GOOD] (define-fun s39 () (_ FloatingPoint  8 24) (_ +oo 8 24))
-[GOOD] (define-fun s41 () String (_ char #x63))
-[GOOD] (define-fun s42 () String "hey")
-[GOOD] (define-fun s44 () (_ FloatingPoint  8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 78.0 1.0)))
-[GOOD] (define-fun s46 () String "tey")
-[GOOD] (define-fun s48 () (_ FloatingPoint  8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 92.0 1.0)))
-[GOOD] (define-fun s50 () String (_ char #x72))
-[GOOD] (define-fun s51 () String "foo")
-[GOOD] (define-fun s53 () (_ FloatingPoint  8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 7.0 2.0)))
-[GOOD] (define-fun s55 () (Seq Int) (seq.++ (seq.unit 1) (seq.unit 2) (seq.unit 3)))
-[GOOD] (define-fun s56 () (Seq (_ FloatingPoint  8 24)) (seq.++ (seq.unit ((_ to_fp 8 24) roundNearestTiesToEven (/ 8598323.0 1048576.0))) (seq.unit ((_ to_fp 8 24) roundNearestTiesToEven (/ 3.0 1.0)))))
-[GOOD] (define-fun s59 () (Seq Int) (seq.++ (seq.unit 9) (seq.unit 5)))
-[GOOD] (define-fun s60 () (Seq (_ FloatingPoint  8 24)) (seq.++ (seq.unit ((_ to_fp 8 24) roundNearestTiesToEven (/ 8598323.0 1048576.0))) (seq.unit ((_ to_fp 8 24) roundNearestTiesToEven (/ 9.0 1.0)))))
-[GOOD] (define-fun s62 () Int 21)
-[GOOD] (define-fun s64 () (Seq Int) (seq.unit 5))
-[GOOD] (define-fun s65 () (Seq (_ FloatingPoint  8 24)) (seq.++ (seq.unit ((_ to_fp 8 24) roundNearestTiesToEven (/ 8598323.0 1048576.0))) (seq.unit (_ +zero 8 24))))
-[GOOD] (define-fun s67 () Int 210)
+[GOOD] (define-fun s21 () Int 5)
+[GOOD] (define-fun s23 () Int 7)
+[GOOD] (define-fun s25 () Int 6)
+[GOOD] (define-fun s29 () (_ FloatingPoint  8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 4508877.0 524288.0)))
+[GOOD] (define-fun s32 () (_ FloatingPoint  8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 5033165.0 524288.0)))
+[GOOD] (define-fun s33 () Int 121)
+[GOOD] (define-fun s38 () Int 8)
+[GOOD] (define-fun s40 () (_ FloatingPoint  8 24) (_ +oo 8 24))
+[GOOD] (define-fun s42 () String (_ char #x63))
+[GOOD] (define-fun s43 () String "hey")
+[GOOD] (define-fun s45 () (_ FloatingPoint  8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 78.0 1.0)))
+[GOOD] (define-fun s47 () String "tey")
+[GOOD] (define-fun s49 () (_ FloatingPoint  8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 92.0 1.0)))
+[GOOD] (define-fun s51 () String (_ char #x72))
+[GOOD] (define-fun s52 () String "foo")
+[GOOD] (define-fun s54 () (_ FloatingPoint  8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 7.0 2.0)))
+[GOOD] (define-fun s56 () (Seq Int) (seq.++ (seq.unit 1) (seq.unit 2) (seq.unit 3)))
+[GOOD] (define-fun s57 () (Seq (_ FloatingPoint  8 24)) (seq.++ (seq.unit ((_ to_fp 8 24) roundNearestTiesToEven (/ 8598323.0 1048576.0))) (seq.unit ((_ to_fp 8 24) roundNearestTiesToEven (/ 3.0 1.0)))))
+[GOOD] (define-fun s60 () (Seq Int) (seq.++ (seq.unit 9) (seq.unit 5)))
+[GOOD] (define-fun s61 () (Seq (_ FloatingPoint  8 24)) (seq.++ (seq.unit ((_ to_fp 8 24) roundNearestTiesToEven (/ 8598323.0 1048576.0))) (seq.unit ((_ to_fp 8 24) roundNearestTiesToEven (/ 9.0 1.0)))))
+[GOOD] (define-fun s63 () Int 21)
+[GOOD] (define-fun s65 () (Seq Int) (seq.unit 5))
+[GOOD] (define-fun s66 () (Seq (_ FloatingPoint  8 24)) (seq.++ (seq.unit ((_ to_fp 8 24) roundNearestTiesToEven (/ 8598323.0 1048576.0))) (seq.unit (_ +zero 8 24))))
+[GOOD] (define-fun s68 () Int 210)
 [GOOD] ; --- top level inputs ---
 [GOOD] (declare-fun s0 () Int)
+[GOOD] (declare-fun s17 () Bool) ; tracks user variable "__internal_sbv_s17"
+[GOOD] (declare-fun s18 () Int) ; tracks user variable "__internal_sbv_s18"
+[GOOD] (declare-fun s70 () Int) ; tracks user variable "__internal_sbv_s70"
 [GOOD] ; --- constant tables ---
 [GOOD] ; --- non-constant tables ---
 [GOOD] ; --- uninterpreted constants ---
@@ -67,52 +69,52 @@
 [GOOD] (define-fun s13 () Int (q1 s0))
 [GOOD] (define-fun s15 () Int (+ s0 s14))
 [GOOD] (define-fun s16 () Bool (= s13 s15))
-[GOOD] (define-fun s18 () Int (q2 false s17))
-[GOOD] (define-fun s19 () Int (q2 true s5))
-[GOOD] (define-fun s21 () Bool (= s19 s20))
-[GOOD] (define-fun s23 () Int (q2 false s22))
-[GOOD] (define-fun s25 () Bool (= s23 s24))
-[GOOD] (define-fun s26 () Int (q2 false s3))
-[GOOD] (define-fun s27 () Bool (= s5 s26))
-[GOOD] (define-fun s29 () (_ FloatingPoint  8 24) (q3 s28 true s3))
-[GOOD] (define-fun s30 () Bool (fp.eq s28 s29))
-[GOOD] (define-fun s33 () (_ FloatingPoint  8 24) (q3 s31 true s32))
-[GOOD] (define-fun s34 () Bool (fp.isZero s33))
-[GOOD] (define-fun s35 () Bool (fp.isNegative s33))
-[GOOD] (define-fun s36 () Bool (and s34 s35))
-[GOOD] (define-fun s38 () (_ FloatingPoint  8 24) (q3 s31 false s37))
-[GOOD] (define-fun s40 () Bool (fp.eq s38 s39))
-[GOOD] (define-fun s43 () (_ FloatingPoint  8 24) (q4 s41 s42))
-[GOOD] (define-fun s45 () Bool (fp.eq s43 s44))
-[GOOD] (define-fun s47 () (_ FloatingPoint  8 24) (q4 s41 s46))
-[GOOD] (define-fun s49 () Bool (fp.eq s47 s48))
-[GOOD] (define-fun s52 () (_ FloatingPoint  8 24) (q4 s50 s51))
-[GOOD] (define-fun s54 () Bool (fp.eq s52 s53))
-[GOOD] (define-fun s57 () Int (q5 s55 s56))
-[GOOD] (define-fun s58 () Bool (= s22 s57))
-[GOOD] (define-fun s61 () Int (q5 s59 s60))
-[GOOD] (define-fun s63 () Bool (= s61 s62))
-[GOOD] (define-fun s66 () Int (q5 s64 s65))
-[GOOD] (define-fun s68 () Bool (= s66 s67))
-[GOOD] (define-fun s69 () Bool (q6 s17))
+[GOOD] (define-fun s19 () Int (q2 s17 s18))
+[GOOD] (define-fun s20 () Int (q2 true s5))
+[GOOD] (define-fun s22 () Bool (= s20 s21))
+[GOOD] (define-fun s24 () Int (q2 false s23))
+[GOOD] (define-fun s26 () Bool (= s24 s25))
+[GOOD] (define-fun s27 () Int (q2 false s3))
+[GOOD] (define-fun s28 () Bool (= s5 s27))
+[GOOD] (define-fun s30 () (_ FloatingPoint  8 24) (q3 s29 true s3))
+[GOOD] (define-fun s31 () Bool (fp.eq s29 s30))
+[GOOD] (define-fun s34 () (_ FloatingPoint  8 24) (q3 s32 true s33))
+[GOOD] (define-fun s35 () Bool (fp.isZero s34))
+[GOOD] (define-fun s36 () Bool (fp.isNegative s34))
+[GOOD] (define-fun s37 () Bool (and s35 s36))
+[GOOD] (define-fun s39 () (_ FloatingPoint  8 24) (q3 s32 false s38))
+[GOOD] (define-fun s41 () Bool (fp.eq s39 s40))
+[GOOD] (define-fun s44 () (_ FloatingPoint  8 24) (q4 s42 s43))
+[GOOD] (define-fun s46 () Bool (fp.eq s44 s45))
+[GOOD] (define-fun s48 () (_ FloatingPoint  8 24) (q4 s42 s47))
+[GOOD] (define-fun s50 () Bool (fp.eq s48 s49))
+[GOOD] (define-fun s53 () (_ FloatingPoint  8 24) (q4 s51 s52))
+[GOOD] (define-fun s55 () Bool (fp.eq s53 s54))
+[GOOD] (define-fun s58 () Int (q5 s56 s57))
+[GOOD] (define-fun s59 () Bool (= s23 s58))
+[GOOD] (define-fun s62 () Int (q5 s60 s61))
+[GOOD] (define-fun s64 () Bool (= s62 s63))
+[GOOD] (define-fun s67 () Int (q5 s65 s66))
+[GOOD] (define-fun s69 () Bool (= s67 s68))
+[GOOD] (define-fun s71 () Bool (q6 s70))
 [GOOD] ; --- delayedEqualities ---
 [GOOD] ; --- formula ---
 [GOOD] (assert s4)
 [GOOD] (assert s8)
 [GOOD] (assert s12)
 [GOOD] (assert s16)
-[GOOD] (assert s21)
-[GOOD] (assert s25)
-[GOOD] (assert s27)
-[GOOD] (assert s30)
-[GOOD] (assert s36)
-[GOOD] (assert s40)
-[GOOD] (assert s45)
-[GOOD] (assert s49)
-[GOOD] (assert s54)
-[GOOD] (assert s58)
-[GOOD] (assert s63)
-[GOOD] (assert s68)
+[GOOD] (assert s22)
+[GOOD] (assert s26)
+[GOOD] (assert s28)
+[GOOD] (assert s31)
+[GOOD] (assert s37)
+[GOOD] (assert s41)
+[GOOD] (assert s46)
+[GOOD] (assert s50)
+[GOOD] (assert s55)
+[GOOD] (assert s59)
+[GOOD] (assert s64)
+[GOOD] (assert s69)
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (q1))

diff --git a/SBVTestSuite/GoldFiles/uiSat_test1.gold b/SBVTestSuite/GoldFiles/uiSat_test1.gold
@@ -11,13 +11,14 @@
 [GOOD] ; --- sums ---
 [GOOD] ; --- literal constants ---
 [GOOD] ; --- top level inputs ---
+[GOOD] (declare-fun s0 () Bool) ; tracks user variable "__internal_sbv_s0"
 [GOOD] ; --- constant tables ---
 [GOOD] ; --- non-constant tables ---
 [GOOD] ; --- uninterpreted constants ---
 [GOOD] (declare-fun q1 (Bool) Bool)
 [GOOD] ; --- user defined functions ---
 [GOOD] ; --- assignments ---
-[GOOD] (define-fun s0 () Bool (q1 false))
+[GOOD] (define-fun s1 () Bool (q1 s0))
 [GOOD] ; --- delayedEqualities ---
 [GOOD] ; --- formula ---
 *** Checking Satisfiability, all solutions..

diff --git a/SBVTestSuite/GoldFiles/uiSat_test2.gold b/SBVTestSuite/GoldFiles/uiSat_test2.gold
@@ -11,13 +11,15 @@
 [GOOD] ; --- sums ---
 [GOOD] ; --- literal constants ---
 [GOOD] ; --- top level inputs ---
+[GOOD] (declare-fun s0 () Bool) ; tracks user variable "__internal_sbv_s0"
+[GOOD] (declare-fun s1 () Bool) ; tracks user variable "__internal_sbv_s1"
 [GOOD] ; --- constant tables ---
 [GOOD] ; --- non-constant tables ---
 [GOOD] ; --- uninterpreted constants ---
 [GOOD] (declare-fun q2 (Bool Bool) Bool)
 [GOOD] ; --- user defined functions ---
 [GOOD] ; --- assignments ---
-[GOOD] (define-fun s0 () Bool (q2 false false))
+[GOOD] (define-fun s2 () Bool (q2 s0 s1))
 [GOOD] ; --- delayedEqualities ---
 [GOOD] ; --- formula ---
 *** Checking Satisfiability, all solutions..

diff --git a/SBVTestSuite/GoldFiles/uiSat_test3.gold b/SBVTestSuite/GoldFiles/uiSat_test3.gold
@@ -11,15 +11,18 @@
 [GOOD] ; --- sums ---
 [GOOD] ; --- literal constants ---
 [GOOD] ; --- top level inputs ---
+[GOOD] (declare-fun s0 () Bool) ; tracks user variable "__internal_sbv_s0"
+[GOOD] (declare-fun s2 () Bool) ; tracks user variable "__internal_sbv_s2"
+[GOOD] (declare-fun s3 () Bool) ; tracks user variable "__internal_sbv_s3"
 [GOOD] ; --- constant tables ---
 [GOOD] ; --- non-constant tables ---
 [GOOD] ; --- uninterpreted constants ---
 [GOOD] (declare-fun q1 (Bool) Bool)
 [GOOD] (declare-fun q2 (Bool Bool) Bool)
 [GOOD] ; --- user defined functions ---
 [GOOD] ; --- assignments ---
-[GOOD] (define-fun s0 () Bool (q1 false))
-[GOOD] (define-fun s1 () Bool (q2 false false))
+[GOOD] (define-fun s1 () Bool (q1 s0))
+[GOOD] (define-fun s4 () Bool (q2 s2 s3))
 [GOOD] ; --- delayedEqualities ---
 [GOOD] ; --- formula ---
 *** Checking Satisfiability, all solutions..