diff --git a/CHANGES.md b/CHANGES.md
index e2dbcbe4db..99380cb3f7 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -24,6 +24,9 @@ A new `enable_lax_pointer_ordering` function exists, which relaxes the
 restrictions that Crucible imposes on comparisons between pointers from
 different allocation blocks.
 
+A SAW value of type `Bool` can now be brought into scope in Cryptol expressions
+as a value of type `Bit`.
+
 ## Changes
 
 * The linked-in version of ABC (based on the Haskell `abcBridge`
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
index 419ad2ef39..7b849795f6 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/Implication.hs
@@ -4101,7 +4101,6 @@ implIntroOrShapeMultiM x bp (sh1 : shs) i =
 implIntroOrShapeMultiM _ _ _ _ = error "implIntroOrShapeMultiM"
 
 
-
 ----------------------------------------------------------------------
 -- * Support for Proving Lifetimes Are Current
 ----------------------------------------------------------------------
diff --git a/intTests/test1404/test.saw b/intTests/test1404/test.saw
new file mode 100644
index 0000000000..f290eaa69e
--- /dev/null
+++ b/intTests/test1404/test.saw
@@ -0,0 +1,2 @@
+let b = true;
+print {{ b }};
diff --git a/intTests/test1404/test.sh b/intTests/test1404/test.sh
new file mode 100644
index 0000000000..2315cc233c
--- /dev/null
+++ b/intTests/test1404/test.sh
@@ -0,0 +1,3 @@
+set -e
+
+$SAW test.saw
diff --git a/src/SAWScript/Value.hs b/src/SAWScript/Value.hs
index c884483ed2..7748fc78a5 100644
--- a/src/SAWScript/Value.hs
+++ b/src/SAWScript/Value.hs
@@ -574,6 +574,9 @@ extendEnv sc x mt md v rw =
          VString s ->
            do tt <- typedTermOfString sc (unpack s)
               pure $ CEnv.bindTypedTerm (ident, tt) ce
+         VBool b ->
+           do tt <- typedTermOfBool sc b
+              pure $ CEnv.bindTypedTerm (ident, tt) ce
          _ ->
            pure ce
      pure $
@@ -590,7 +593,7 @@ extendEnv sc x mt md v rw =
 
 typedTermOfString :: SharedContext -> String -> IO TypedTerm
 typedTermOfString sc str =
-  do let schema = Cryptol.Forall [] [] (Cryptol.tString (length str))
+  do let schema = Cryptol.tMono (Cryptol.tString (length str))
      bvNat <- scGlobalDef sc "Prelude.bvNat"
      bvNat8 <- scApply sc bvNat =<< scNat sc 8
      byteT <- scBitvector sc 8
@@ -599,6 +602,12 @@ typedTermOfString sc str =
      trm <- scVector sc byteT ts
      pure (TypedTerm (TypedTermSchema schema) trm)
 
+typedTermOfBool :: SharedContext -> Bool -> IO TypedTerm
+typedTermOfBool sc b =
+  do let schema = Cryptol.tMono Cryptol.tBit
+     trm <- scBool sc b
+     pure (TypedTerm (TypedTermSchema schema) trm)
+
 
 -- Other SAWScript Monads ------------------------------------------------------