diff --git a/src/ansi-c/library/pthread_lib.c b/src/ansi-c/library/pthread_lib.c
index 71af169c91b..b2be1cd02ae 100644
--- a/src/ansi-c/library/pthread_lib.c
+++ b/src/ansi-c/library/pthread_lib.c
@@ -534,11 +534,8 @@ inline int pthread_create(
   this_thread_id=++__CPROVER_next_thread_id;
   __CPROVER_atomic_end();
 
-  if(thread)
-  {
-    // pthread_t is a pointer type on some systems
-    *thread=(pthread_t)this_thread_id;
-  }
+  // pthread_t is a pointer type on some systems
+  *thread=(pthread_t)this_thread_id;
 
   #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
   __CPROVER_set_must(thread, "pthread-id");
diff --git a/src/ansi-c/library/string.c b/src/ansi-c/library/string.c
index 35cf46f7f66..07d70f9807f 100644
--- a/src/ansi-c/library/string.c
+++ b/src/ansi-c/library/string.c
@@ -299,7 +299,7 @@ inline int strcmp(const char *s1, const char *s2)
 {
   __CPROVER_HIDE:;
   #if !defined(__linux__) || defined(__GLIBC__)
-  if(s1!=0 && s1==s2) return 0;
+  if(s1==s2) return 0;
   #else
   // musl guarantees non-null of s1
   if(s1==s2) return 0;
@@ -346,7 +346,7 @@ inline int strcasecmp(const char *s1, const char *s2)
 {
   __CPROVER_HIDE:;
   #if !defined(__linux__) || defined(__GLIBC__)
-  if(s1!=0 && s1==s2) return 0;
+  if(s1==s2) return 0;
   #else
   // musl guarantees non-null of s1
   if(s1==s2) return 0;
@@ -396,7 +396,7 @@ inline int strncmp(const char *s1, const char *s2, size_t n)
 {
   __CPROVER_HIDE:;
   #if !defined(__linux__) || defined(__GLIBC__)
-  if(s1!=0 && s1==s2) return 0;
+  if(s1==s2) return 0;
   #else
   // musl guarantees non-null of s1
   if(s1==s2) return 0;
@@ -440,7 +440,7 @@ inline int strncasecmp(const char *s1, const char *s2, size_t n)
 {
   __CPROVER_HIDE:;
   #if !defined(__linux__) || defined(__GLIBC__)
-  if(s1!=0 && s1==s2) return 0;
+  if(s1==s2) return 0;
   #else
   // musl guarantees non-null of s1
   if(s1==s2) return 0;