Use safeSymbol instead of userSymbol to avoid an error case.

GaloisInc · Nov 3, 2020 · 47f6264 · 47f6264
1 parent 7b6167e
commit 47f6264
Showing 1 changed file with 1 addition and 4 deletions.
diff --git a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs
@@ -953,10 +953,7 @@ mkConstant ::
   forall sym ty.
   (IsSymExprBuilder sym) =>
   sym -> String -> BaseTypeRepr ty -> IO (SymExpr sym ty)
-mkConstant sym name ty =
-  case W.userSymbol name of
-    Right solverSymbol -> W.freshConstant sym solverSymbol ty
-    Left _ -> fail $ "Cannot create solver symbol " ++ name
+mkConstant sym name ty = W.freshConstant sym (W.safeSymbol name) ty
 
 -- | Generate a new variable from a given BaseType