diff --git a/Data/SBV.hs b/Data/SBV.hs
index a19d2c487..11280cb38 100644
--- a/Data/SBV.hs
+++ b/Data/SBV.hs
@@ -113,7 +113,7 @@
 -- all satisfying assignments.
 --
 -- The sbv library uses third-party SMT solvers via the standard SMT-Lib interface:
--- <http://smtlib.cs.uiowa.edu/>
+-- <https://smt-lib.org>
 --
 -- The SBV library is designed to work with any SMT-Lib compliant SMT-solver.
 -- Currently, we support the following SMT-Solvers out-of-the box:
@@ -541,7 +541,7 @@ The SBV library provides a "push-button" verification system via automated SMT s
 design goal is to let SMT solvers be used without any knowledge of how SMT solvers work
 or how different logics operate. The details are hidden behind the SBV framework, providing
 Haskell programmers with a clean API that is unencumbered by the details of individual solvers.
-To that end, we use the SMT-Lib standard (<http://smtlib.cs.uiowa.edu/>)
+To that end, we use the SMT-Lib standard (<https://smt-lib.org>)
 to communicate with arbitrary SMT solvers.
 -}
 
@@ -788,7 +788,7 @@ represent transcendentals.) Some irrational numbers are algebraic (such as @sqrt
 others are not (such as pi and e).
 
 SBV can deal with real numbers just fine, since the theory of reals is decidable. (See
-<http://smtlib.cs.uiowa.edu/theories-Reals.shtml>.) In addition, by leveraging backend
+<https://smt-lib.org/theories-Reals.shtml>.) In addition, by leveraging backend
 solver capabilities, SBV can also represent and solve non-linear equations involving real-variables.
 (For instance, the Z3 SMT solver, supports polynomial constraints on reals starting with v4.0.)
 -}
diff --git a/Data/SBV/Control/Types.hs b/Data/SBV/Control/Types.hs
index e4fe0fe54..67a1958a2 100644
--- a/Data/SBV/Control/Types.hs
+++ b/Data/SBV/Control/Types.hs
@@ -84,7 +84,7 @@ instance Show SMTInfoFlag where
   show Version              = ":version"
   show (InfoKeyword s)      = s
 
--- | Option values that can be set in the solver, following the SMTLib specification <http://smtlib.cs.uiowa.edu/language.shtml>.
+-- | Option values that can be set in the solver, following the SMTLib specification <https://smt-lib.org/language.shtml>.
 --
 -- Note that not all solvers may support all of these!
 --
@@ -183,7 +183,7 @@ setSMTOption = cvt
 
 -- | SMT-Lib logics. If left unspecified SBV will pick the logic based on what it determines is needed. However, the
 -- user can override this choice using a call to 'Data.SBV.setLogic' This is especially handy if one is experimenting with custom
--- logics that might be supported on new solvers. See <http://smtlib.cs.uiowa.edu/logics.shtml> for the official list.
+-- logics that might be supported on new solvers. See <https://smt-lib.org/logics.shtml> for the official list.
 data Logic
   = AUFLIA             -- ^ Formulas over the theory of linear integer arithmetic and arrays extended with free sort and function symbols but restricted to arrays with integer indices and values.
   | AUFLIRA            -- ^ Linear formulas with free sort and function symbols over one- and two-dimentional arrays of integer index and real value.