GaloisInc · brianhuffman · Dec 4, 2020 · Nov 25, 2020 · Dec 3, 2020 · Dec 4, 2020
diff --git a/cabal.GHC-8.6.5.config b/cabal.GHC-8.6.5.config
@@ -22,8 +22,6 @@ constraints: any.Cabal ==2.4.0.1,
              alex +small_base,
              any.ansi-terminal ==0.10.3,
              ansi-terminal -example,
-             any.ansi-wl-pprint ==0.6.9,
-             ansi-wl-pprint -example,
              any.array ==0.5.3.0,
              any.assoc ==1.0.1,
              any.async ==2.2.2,

diff --git a/cabal.GHC-8.8.3.config b/cabal.GHC-8.8.3.config
@@ -22,8 +22,6 @@ constraints: any.Cabal ==3.0.1.0,
              alex +small_base,
              any.ansi-terminal ==0.10.3,
              ansi-terminal -example,
-             any.ansi-wl-pprint ==0.6.9,
-             ansi-wl-pprint -example,
              any.array ==0.5.4.0,
              any.assoc ==1.0.1,
              any.async ==2.2.2,

diff --git a/cabal.GHC-8.8.4.config b/cabal.GHC-8.8.4.config
@@ -22,8 +22,6 @@ constraints: any.Cabal ==3.0.1.0,
              alex +small_base,
              any.ansi-terminal ==0.10.3,
              ansi-terminal -example,
-             any.ansi-wl-pprint ==0.6.9,
-             ansi-wl-pprint -example,
              any.array ==0.5.4.0,
              any.assoc ==1.0.1,
              any.async ==2.2.2,

diff --git a/deps/crucible b/deps/crucible
diff --git a/deps/elf-edit b/deps/elf-edit
diff --git a/deps/macaw b/deps/macaw
diff --git a/deps/what4 b/deps/what4
diff --git a/saw-script.cabal b/saw-script.cabal
@@ -28,7 +28,6 @@ library
   build-depends:
       base >= 4
     , aig
-    , ansi-wl-pprint
     , array
     , binary
     , bimap

diff --git a/src/SAWScript/AST.hs b/src/SAWScript/AST.hs
@@ -7,6 +7,7 @@ Stability   : provisional
 -}
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE DeriveFunctor,DeriveFoldable,DeriveTraversable #-}
+{-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE LambdaCase #-}
@@ -47,11 +48,11 @@ import Data.List (intercalate)
 import Data.Foldable (Foldable)
 import Data.Traversable (Traversable)
 #endif
-import qualified Text.PrettyPrint.ANSI.Leijen as PP
-import           Text.PrettyPrint.ANSI.Leijen (Pretty)
+import qualified Prettyprinter as PP
+import           Prettyprinter (Pretty)
 
 import qualified Cryptol.Parser.AST as P (ImportSpec(..), ModName)
-import qualified Cryptol.Utils.Ident as P (unpackIdent, modNameChunks)
+import qualified Cryptol.Utils.Ident as P (identText, modNameChunks)
 
 -- Names {{{
 
@@ -218,53 +219,56 @@ data Schema = Forall [Name] Type
 
 -- Pretty Printing {{{
 
-prettyWholeModule :: [Stmt] -> PP.Doc
-prettyWholeModule = (PP.<> PP.linebreak) . vcatWithSemi . map PP.pretty
+prettyWholeModule :: [Stmt] -> PP.Doc ann
+prettyWholeModule = (PP.<> PP.line') . vcatWithSemi . map PP.pretty
 
-vcatWithSemi :: [PP.Doc] -> PP.Doc
+vcatWithSemi :: [PP.Doc ann] -> PP.Doc ann
 vcatWithSemi = PP.vcat . map (PP.<> PP.semi)
 
 instance Pretty Expr where
   pretty expr0 = case expr0 of
-    Bool b   -> PP.text $ show b
-    String s -> PP.dquotes (PP.text s)
-    Int i    -> PP.integer i
-    Code ls  -> PP.braces . PP.braces $ PP.text (getVal ls)
-    CType (Located string _ _) -> PP.braces . PP.text $ "|" ++ string ++ "|"
+    Bool b   -> PP.viaShow b
+    String s -> PP.dquotes (PP.pretty s)
+    Int i    -> PP.pretty i
+    Code ls  -> PP.braces . PP.braces $ PP.pretty (getVal ls)
+    CType (Located string _ _) -> PP.braces . PP.pretty $ "|" ++ string ++ "|"
     Array xs -> PP.list (map PP.pretty xs)
     Block stmts ->
-      PP.text "do" PP.<+> PP.lbrace PP.<> PP.linebreak PP.<>
+      "do" PP.<+> PP.lbrace PP.<> PP.line' PP.<>
       (PP.indent 3 $ (PP.align . vcatWithSemi . map PP.pretty $ stmts)) PP.<>
-      PP.linebreak PP.<> PP.rbrace
+      PP.line' PP.<> PP.rbrace
     Tuple exprs -> PP.tupled (map PP.pretty exprs)
     Record mapping ->
       PP.braces . (PP.space PP.<>) . (PP.<> PP.space) . PP.align . PP.sep . PP.punctuate PP.comma $
-      map (\(name, value) -> PP.text name PP.<+> PP.text "=" PP.<+> PP.pretty value)
+      map (\(name, value) -> PP.pretty name PP.<+> "=" PP.<+> PP.pretty value)
       (Map.assocs mapping)
     Index _ _ -> error "No concrete syntax for AST node 'Index'"
-    Lookup expr name -> PP.pretty expr PP.<> PP.dot PP.<> PP.text name
-    TLookup expr int -> PP.pretty expr PP.<> PP.dot PP.<> PP.integer int
+    Lookup expr name -> PP.pretty expr PP.<> PP.dot PP.<> PP.pretty name
+    TLookup expr int -> PP.pretty expr PP.<> PP.dot PP.<> PP.pretty int
     Var (Located name _ _) ->
-      PP.text name
+      PP.pretty name
     Function pat expr ->
-      PP.text "\\" PP.<+> PP.pretty pat PP.<+> PP.text "-> " PP.<+> PP.pretty expr
+      "\\" PP.<+> PP.pretty pat PP.<+> "-> " PP.<+> PP.pretty expr
     -- FIXME, use precedence to minimize parentheses
     Application f a -> PP.parens (PP.pretty f PP.<+> PP.pretty a)
     Let (NonRecursive decl) expr ->
-      PP.text "let" PP.<+>
-      prettyDef decl PP.</>
-      PP.text "in" PP.<+> PP.pretty expr
+      PP.fillSep
+      [ "let" PP.<+> prettyDef decl
+      , "in" PP.<+> PP.pretty expr
+      ]
     Let (Recursive decls) expr ->
-      PP.text "let" PP.<+>
-      PP.cat (PP.punctuate
-              (PP.empty PP.</> PP.text "and" PP.<> PP.space)
-              (map prettyDef decls)) PP.</>
-      PP.text "in" PP.<+> PP.pretty expr
+      PP.fillSep
+      [ "let" PP.<+>
+        PP.cat (PP.punctuate
+                (PP.fillSep [PP.emptyDoc, "and" PP.<> PP.space])
+                (map prettyDef decls))
+      , "in" PP.<+> PP.pretty expr
+      ]
     TSig expr typ -> PP.parens $ PP.pretty expr PP.<+> PP.colon PP.<+> pretty 0 typ
     IfThenElse e1 e2 e3 ->
-      PP.text "if" PP.<+> PP.pretty e1 PP.<+>
-      PP.text "then" PP.<+> PP.pretty e2 PP.<+>
-      PP.text "else" PP.<+> PP.pretty e3
+      "if" PP.<+> PP.pretty e1 PP.<+>
+      "then" PP.<+> PP.pretty e2 PP.<+>
+      "else" PP.<+> PP.pretty e3
     LExpr _ e -> PP.pretty e
 
 instance PrettyPrint Expr where
@@ -285,57 +289,57 @@ instance Pretty Stmt where
       StmtBind _ (PWild _leftType) _rightType expr ->
          PP.pretty expr
       StmtBind _ pat _rightType expr ->
-         PP.pretty pat PP.<+> PP.text "<-" PP.<+> PP.align (PP.pretty expr)
+         PP.pretty pat PP.<+> "<-" PP.<+> PP.align (PP.pretty expr)
       StmtLet _ (NonRecursive decl) ->
-         PP.text "let" PP.<+> prettyDef decl
+         "let" PP.<+> prettyDef decl
       StmtLet _ (Recursive decls) ->
-         PP.text "rec" PP.<+>
+         "rec" PP.<+>
          PP.cat (PP.punctuate
-            (PP.empty PP.</> PP.text "and" PP.<> PP.space)
+            (PP.fillSep [PP.emptyDoc, "and" PP.<> PP.space])
             (map prettyDef decls))
       StmtCode _ (Located code _ _) ->
-         PP.text "let" PP.<+>
-            (PP.braces . PP.braces $ PP.text code)
+         "let" PP.<+>
+            (PP.braces . PP.braces $ PP.pretty code)
       StmtImport _ Import{iModule,iAs,iSpec} ->
-         PP.text "import" PP.<+>
+         "import" PP.<+>
          (case iModule of
             Left filepath ->
-               PP.dquotes . PP.text $ filepath
+               PP.dquotes . PP.pretty $ filepath
             Right modName ->
                ppModName modName) PP.<>
          (case iAs of
             Just modName ->
-               PP.space PP.<> PP.text "as" PP.<+> ppModName modName
-            Nothing -> PP.empty) PP.<>
+               PP.space PP.<> "as" PP.<+> ppModName modName
+            Nothing -> PP.emptyDoc) PP.<>
          (case iSpec of
             Just (P.Hiding names) ->
-               PP.space PP.<> PP.text "hiding" PP.<+> PP.tupled (map ppIdent names)
+               PP.space PP.<> "hiding" PP.<+> PP.tupled (map ppIdent names)
             Just (P.Only names) ->
                PP.space PP.<> PP.tupled (map ppIdent names)
-            Nothing -> PP.empty)
+            Nothing -> PP.emptyDoc)
       StmtTypedef _ (Located name _ _) ty ->
-         PP.text "typedef" PP.<+> PP.text name PP.<+> pretty 0 ty
-      --expr -> PP.cyan . PP.text $ show expr
+         "typedef" PP.<+> PP.pretty name PP.<+> pretty 0 ty
+      --expr -> PP.cyan . PP.viaShow expr
 
       where
-        ppModName mn = PP.text (intercalate "." (P.modNameChunks mn))
-        ppIdent i = PP.text (P.unpackIdent i)
+        ppModName mn = PP.pretty (intercalate "." (P.modNameChunks mn))
+        ppIdent i = PP.pretty (P.identText i)
         --ppName n = ppIdent (P.nameIdent n)
 
-prettyDef :: Decl -> PP.Doc
+prettyDef :: Decl -> PP.Doc ann
 prettyDef (Decl _ pat _ def) =
    PP.pretty pat PP.<+>
    let (args, body) = dissectLambda def
    in (if not (null args)
           then PP.hsep (map PP.pretty args) PP.<> PP.space
-          else PP.empty) PP.<>
-      PP.text "=" PP.<+> PP.pretty body
+          else PP.emptyDoc) PP.<>
+      "=" PP.<+> PP.pretty body
 
-prettyMaybeTypedArg :: (Name,Maybe Type) -> PP.Doc
+prettyMaybeTypedArg :: (Name, Maybe Type) -> PP.Doc ann
 prettyMaybeTypedArg (name,Nothing) =
-   PP.text name
+   PP.pretty name
 prettyMaybeTypedArg (name,Just typ) =
-   PP.parens $ PP.text name PP.<+> PP.colon PP.<+> pretty 0 typ
+   PP.parens $ PP.pretty name PP.<+> PP.colon PP.<+> pretty 0 typ
 
 dissectLambda :: Expr -> ([Pattern], Expr)
 dissectLambda = \case
@@ -346,71 +350,71 @@ pShow :: PrettyPrint a => a -> String
 pShow = show . pretty 0
 
 class PrettyPrint p where
-  pretty :: Int -> p -> PP.Doc
+  pretty :: Int -> p -> PP.Doc ann
 
 instance PrettyPrint Schema where
   pretty _ (Forall ns t) = case ns of
     [] -> pretty 0 t
-    _  -> PP.braces (commaSepAll $ map PP.text ns) PP.<+> pretty 0 t
+    _  -> PP.braces (commaSepAll $ map PP.pretty ns) PP.<+> pretty 0 t
 
 instance PrettyPrint Type where
   pretty par t@(TyCon tc ts) = case (tc,ts) of
     (_,[])                 -> pretty par tc
     (TupleCon _,_)         -> PP.parens $ commaSepAll $ map (pretty 0) ts
     (ArrayCon,[typ])       -> PP.brackets (pretty 0 typ)
     (FunCon,[f,v])         -> (if par > 0 then PP.parens else id) $
-                                pretty 1 f PP.<+> PP.text "->" PP.<+> pretty 0 v
+                                pretty 1 f PP.<+> "->" PP.<+> pretty 0 v
     (BlockCon,[cxt,typ])   -> (if par > 1 then PP.parens else id) $
                                 pretty 1 cxt PP.<+> pretty 2 typ
     _ -> error $ "malformed TyCon: " ++ show t
   pretty _par (TyRecord fs) =
       PP.braces
     $ commaSepAll
-    $ map (\(n,t) -> PP.text n `prettyTypeSig` pretty 0 t)
+    $ map (\(n,t) -> PP.pretty n `prettyTypeSig` pretty 0 t)
     $ Map.toList fs
-  pretty _par (TyUnifyVar i)    = PP.text "t." PP.<> PP.integer i
-  pretty _par (TySkolemVar n i) = PP.text n PP.<> PP.integer i
-  pretty _par (TyVar n)         = PP.text n
+  pretty _par (TyUnifyVar i)    = "t." PP.<> PP.pretty i
+  pretty _par (TySkolemVar n i) = PP.pretty n PP.<> PP.pretty i
+  pretty _par (TyVar n)         = PP.pretty n
   pretty par (LType _ t)        = pretty par t
 
 instance PrettyPrint TyCon where
   pretty par tc = case tc of
-    TupleCon n     -> PP.parens $ replicateDoc (n - 1) $ PP.char ','
-    ArrayCon       -> PP.parens $ PP.brackets $ PP.empty
-    FunCon         -> PP.parens $ PP.text "->"
-    StringCon      -> PP.text "String"
-    TermCon        -> PP.text "Term"
-    TypeCon        -> PP.text "Type"
-    BoolCon        -> PP.text "Bool"
-    IntCon         -> PP.text "Int"
-    AIGCon         -> PP.text "AIG"
-    CFGCon         -> PP.text "CFG"
-    BlockCon       -> PP.text "<Block>"
+    TupleCon n     -> PP.parens $ replicateDoc (n - 1) $ PP.pretty ','
+    ArrayCon       -> PP.parens $ PP.brackets $ PP.emptyDoc
+    FunCon         -> PP.parens $ "->"
+    StringCon      -> "String"
+    TermCon        -> "Term"
+    TypeCon        -> "Type"
+    BoolCon        -> "Bool"
+    IntCon         -> "Int"
+    AIGCon         -> "AIG"
+    CFGCon         -> "CFG"
+    BlockCon       -> "<Block>"
     ContextCon cxt -> pretty par cxt
 
 instance PrettyPrint Context where
   pretty _ c = case c of
-    CryptolSetup -> PP.text "CryptolSetup"
-    JavaSetup    -> PP.text "JavaSetup"
-    LLVMSetup    -> PP.text "LLVMSetup"
-    ProofScript  -> PP.text "ProofScript"
-    TopLevel     -> PP.text "TopLevel"
-    CrucibleSetup-> PP.text "CrucibleSetup"
-
-replicateDoc :: Integer -> PP.Doc -> PP.Doc
+    CryptolSetup -> "CryptolSetup"
+    JavaSetup    -> "JavaSetup"
+    LLVMSetup    -> "LLVMSetup"
+    ProofScript  -> "ProofScript"
+    TopLevel     -> "TopLevel"
+    CrucibleSetup-> "CrucibleSetup"
+
+replicateDoc :: Integer -> PP.Doc ann -> PP.Doc ann
 replicateDoc n d
-  | n < 1 = PP.empty
+  | n < 1 = PP.emptyDoc
   | True  = d PP.<> replicateDoc (n-1) d
 
-prettyTypeSig :: PP.Doc -> PP.Doc -> PP.Doc
-prettyTypeSig n t = n PP.<+> PP.char ':' PP.<+> t
+prettyTypeSig :: PP.Doc ann -> PP.Doc ann -> PP.Doc ann
+prettyTypeSig n t = n PP.<+> PP.pretty ':' PP.<+> t
 
-commaSep :: PP.Doc -> PP.Doc -> PP.Doc
+commaSep :: PP.Doc ann -> PP.Doc ann -> PP.Doc ann
 commaSep = ((PP.<+>) . (PP.<> PP.comma))
 
-commaSepAll :: [PP.Doc] -> PP.Doc
+commaSepAll :: [PP.Doc ann] -> PP.Doc ann
 commaSepAll ds = case ds of
-  [] -> PP.empty
+  [] -> PP.emptyDoc
   _  -> foldl1 commaSep ds
 
 -- }}}

diff --git a/src/SAWScript/AutoMatch.hs b/src/SAWScript/AutoMatch.hs
@@ -59,7 +59,7 @@ import SAWScript.LLVMBuiltins
 --import SAWScript.JavaBuiltins
 import Language.JVM.Common (dotsToSlashes, mkClassName)
 
-import Text.PrettyPrint.ANSI.Leijen (putDoc, hPutDoc)
+import Prettyprinter.Render.Text (putDoc, hPutDoc)
 
 import System.IO
 

diff --git a/src/SAWScript/Crucible/Common.hs b/src/SAWScript/Crucible/Common.hs
@@ -27,30 +27,33 @@ import qualified What4.ProgramLoc as W4 (plSourceLoc)
 
 import System.Directory (createDirectoryIfMissing)
 import System.FilePath ((</>))
-import qualified Text.PrettyPrint.ANSI.Leijen as PP hiding ((<$>), (<>))
+import qualified Prettyprinter as PP
 
 -- | The symbolic backend we use for SAW verification
 type Sym = SAWCoreBackend Nonce.GlobalNonceGenerator Yices.Connection (W4.Flags W4.FloatReal)
 
-ppAbortedResult :: (forall l args. GlobalPair Sym (SimFrame Sym ext l args) -> PP.Doc)
+ppAbortedResult :: (forall l args. GlobalPair Sym (SimFrame Sym ext l args) -> PP.Doc ann)
                 -> AbortedResult Sym ext
-                -> PP.Doc
+                -> PP.Doc ann
 ppAbortedResult _ (AbortedExec InfeasibleBranch _) =
-  PP.text "Infeasible branch"
+  PP.pretty "Infeasible branch"
 ppAbortedResult ppGP (AbortedExec abt gp) = do
-  ppAbortExecReason abt PP.<$$> ppGP gp
+  PP.vcat
+    [ ppAbortExecReason abt
+    , ppGP gp
+    ]
 ppAbortedResult ppGP (AbortedBranch loc _predicate trueBranch falseBranch) =
   PP.vcat
-    [ PP.text "Both branches aborted after a symbolic branch."
-    , PP.text "Location of control-flow branching:"
-    , PP.indent 2 (PP.text (show (W4.plSourceLoc loc)))
-    , PP.text "Message from the true branch:"
+    [ PP.pretty "Both branches aborted after a symbolic branch."
+    , PP.pretty "Location of control-flow branching:"
+    , PP.indent 2 (PP.pretty (W4.plSourceLoc loc))
+    , PP.pretty "Message from the true branch:"
     , PP.indent 2 (ppAbortedResult ppGP trueBranch)
-    , PP.text "Message from the false branch:"
+    , PP.pretty "Message from the false branch:"
     , PP.indent 2 (ppAbortedResult ppGP falseBranch)
     ]
 ppAbortedResult _ (AbortedExit ec) =
-  PP.text "Branch exited:" PP.<+> PP.text (show ec)
+  PP.pretty "Branch exited:" PP.<+> PP.viaShow ec
 
 setupProfiling ::
   IsSymInterface sym =>
+1 −1		elf-edit.cabal
+27 −24		src/Data/ElfEdit/HighLevel/Types.hs
+2 −2		src/Data/ElfEdit/Prim/SymbolTable.hs
+2 −2		src/Data/ElfEdit/Relocations/Common.hs
+3 −3		src/Data/ElfEdit/Utils.hs
+2 −0		stack-8.4.yaml
+2 −0		stack-8.6.yaml
+1 −1		base/macaw-base.cabal
+44 −33		base/src/Data/Macaw/AbsDomain/AbsState.hs
+9 −8		base/src/Data/Macaw/AbsDomain/JumpBounds.hs
+31 −30		base/src/Data/Macaw/AbsDomain/StackAnalysis.hs
+8 −7		base/src/Data/Macaw/AbsDomain/StridedInterval.hs
+23 −21		base/src/Data/Macaw/Analysis/RegisterUse.hs
+9 −9		base/src/Data/Macaw/CFG/App.hs
+6 −5		base/src/Data/Macaw/CFG/AssignRhs.hs
+13 −9		base/src/Data/Macaw/CFG/Block.hs
+59 −60		base/src/Data/Macaw/CFG/Core.hs
+8 −5		base/src/Data/Macaw/DebugLogging.hs
+1 −1		base/src/Data/Macaw/Discovery.hs
+51 −38		base/src/Data/Macaw/Discovery/State.hs
+43 −41		base/src/Data/Macaw/Dwarf.hs
+11 −10		base/src/Data/Macaw/Memory.hs
+8 −7		base/src/Data/Macaw/Types.hs
+6 −6		base/src/Data/Macaw/Utils/Pretty.hs
+2 −2		cabal.project.dist.ghc-8.10.2.freeze
+2 −2		cabal.project.dist.ghc-8.6.5.freeze
+2 −3		cabal.project.dist.ghc-8.8.4.freeze
+1 −1		deps/asl-translator
+1 −1		deps/crucible
+1 −1		deps/elf-edit
+1 −1		deps/macaw-loader
+1 −1		deps/what4
+2 −2		macaw-aarch32/macaw-aarch32.cabal
+2 −2		macaw-aarch32/src/Data/Macaw/ARM/ARMReg.hs
+11 −10		macaw-aarch32/src/Data/Macaw/ARM/Arch.hs
+3 −3		macaw-aarch32/src/Data/Macaw/ARM/BinaryFormat/ELF.hs
+2 −2		macaw-aarch32/tests/ARMTests.hs
+1 −1		macaw-ppc/macaw-ppc.cabal
+40 −39		macaw-ppc/src/Data/Macaw/PPC/Arch.hs
+1 −1		macaw-ppc/src/Data/Macaw/PPC/Eval.hs
+2 −2		macaw-ppc/src/Data/Macaw/PPC/PPCReg.hs
+0 −1		macaw-semmc/macaw-semmc.cabal
+0 −2		refinement/macaw-refinement.cabal
+2 −3		refinement/src/Data/Macaw/Refinement/Path.hs
+1 −1		symbolic/macaw-symbolic.cabal
+14 −14		symbolic/src/Data/Macaw/Symbolic/CrucGen.hs
+1 −1		x86/macaw-x86.cabal
+2 −2		x86/src/Data/Macaw/X86.hs
+16 −15		x86/src/Data/Macaw/X86/ArchTypes.hs
+2 −2		x86/src/Data/Macaw/X86/Generator.hs
+7 −6		x86/src/Data/Macaw/X86/Monad.hs
+2 −2		x86/src/Data/Macaw/X86/X86Reg.hs
+1 −1		x86_symbolic/macaw-x86-symbolic.cabal
+1 −1		x86_symbolic/src/Data/Macaw/X86/Crucible.hs
+16 −10		what4-abc/src/What4/Solver/ABC.hs
+1 −1		what4-abc/what4-abc.cabal
+11 −7		what4-blt/src/What4/Solver/BLT.hs
+1 −1		what4-blt/what4-blt.cabal
+4 −4		what4/src/What4/BaseTypes.hs
+17 −13		what4/src/What4/Concrete.hs
+56 −49		what4/src/What4/Config.hs
+6 −6		what4/src/What4/Expr/App.hs
+48 −45		what4/src/What4/Expr/Builder.hs
+66 −63		what4/src/What4/Expr/MATLAB.hs
+4 −3		what4/src/What4/Expr/VarIdentification.hs
+2 −2		what4/src/What4/FunctionName.hs
+2 −2		what4/src/What4/Interface.hs
+2 −2		what4/src/What4/InterpretedFloatingPoint.hs
+13 −13		what4/src/What4/ProgramLoc.hs
+3 −3		what4/src/What4/Protocol/Online.hs
+5 −5		what4/src/What4/Protocol/PolyRoot.hs
+20 −16		what4/src/What4/Protocol/SMTLib2.hs
+52 −45		what4/src/What4/Protocol/SMTWriter.hs
+2 −2		what4/src/What4/Solver/Adapter.hs
+1 −2		what4/src/What4/Solver/Boolector.hs
+2 −3		what4/src/What4/Solver/CVC4.hs
+1 −2		what4/src/What4/Solver/DReal.hs
+1 −2		what4/src/What4/Solver/STP.hs
+7 −7		what4/src/What4/Solver/Yices.hs
+2 −3		what4/src/What4/Solver/Z3.hs
+1 −1		what4/what4.cabal