From 59dfb09096cc435122e199f87961551047290e7c Mon Sep 17 00:00:00 2001 From: Matthew Yacavone Date: Mon, 15 Aug 2022 17:03:34 -0700 Subject: [PATCH] revert lifting of uvar ctx in withUVars --- src/SAWScript/Prover/MRSolver/Monad.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/SAWScript/Prover/MRSolver/Monad.hs b/src/SAWScript/Prover/MRSolver/Monad.hs index 9db935e10d..ac62470757 100644 --- a/src/SAWScript/Prover/MRSolver/Monad.hs +++ b/src/SAWScript/Prover/MRSolver/Monad.hs @@ -679,7 +679,7 @@ withUVars :: [(LocalName,Term)] -> ([Term] -> MRM a) -> MRM a withUVars [] f = f [] withUVars ctx f = do nms <- uniquifyNames (map fst ctx) <$> map fst <$> mrUVars - ctx_u <- zip nms <$> mapM (liftTermLike 0 (length ctx) . Type . snd) ctx + let ctx_u = zip nms $ map (Type . snd) ctx assumps' <- mrAssumptions >>= liftTerm 0 (length ctx) dataTypeAssumps' <- mrDataTypeAssumps >>= mapM (liftTermLike 0 (length ctx)) vars <- reverse <$> mapM (liftSC1 scLocalVar) [0 .. length ctx - 1]