diff --git a/ocaml/fstar-lib/FStarC_Parser_LexFStar.ml b/ocaml/fstar-lib/FStarC_Parser_LexFStar.ml
index e4ef505d01f..5943d01b513 100644
--- a/ocaml/fstar-lib/FStarC_Parser_LexFStar.ml
+++ b/ocaml/fstar-lib/FStarC_Parser_LexFStar.ml
@@ -473,6 +473,7 @@ match%sedlex lexbuf with
  | "#print-effects-graph" -> PRAGMA_PRINT_EFFECTS_GRAPH
  | "__SOURCE_FILE__" -> STRING (L.source_file lexbuf)
  | "__LINE__" -> INT (string_of_int (L.current_line lexbuf), false)
+ | "__FL__"   -> STRING ((L.source_file lexbuf) ^ "(" ^ (string_of_int (L.current_line lexbuf)) ^ ")")
 
  | Plus anywhite -> token lexbuf
  | newline -> L.new_line lexbuf; token lexbuf
diff --git a/tests/Makefile b/tests/Makefile
index e864166662f..5476766c02b 100644
--- a/tests/Makefile
+++ b/tests/Makefile
@@ -21,6 +21,7 @@ ALL_TEST_DIRS += vale
 ALL_TEST_DIRS += hacl
 ALL_TEST_DIRS += simple_hello
 ALL_TEST_DIRS += dune_hello
+ALL_TEST_DIRS += validation-time
 HAS_OCAML := $(shell which ocamlfind 2>/dev/null)
 
 ifneq (,$(HAS_OCAML))
diff --git a/tests/validation-time/Makefile b/tests/validation-time/Makefile
new file mode 100644
index 00000000000..01483aa279a
--- /dev/null
+++ b/tests/validation-time/Makefile
@@ -0,0 +1,22 @@
+#
+# This does nothing but the default validation as these are validation time test modules.
+# Most are let _ = assert(...) which is extremely cool to test at validation time! 
+# 
+
+WARN_ERROR=--warn_error -321
+FSTAR_HOME=../..
+FSTAR_FILES=$(wildcard *.fst)
+FSTAR_EXAMPLES=$(realpath ../../examples)
+include $(FSTAR_EXAMPLES)/Makefile.include
+
+all: verify-all
+
+include $(FSTAR_HOME)/examples/Makefile.common
+
+verify-all: $(CACHE_DIR) $(addsuffix .checked, $(addprefix $(CACHE_DIR)/, $(FSTAR_FILES)))
+
+clean:
+	$(call msg, "CLEAN")
+	$(Q)rm -f .depend
+	$(Q)rm -rf _cache
+	$(Q)rm -rf _output
diff --git a/tests/validation-time/README.md b/tests/validation-time/README.md
new file mode 100644
index 00000000000..a0b516b2772
--- /dev/null
+++ b/tests/validation-time/README.md
@@ -0,0 +1,5 @@
+
+  This directory contains tests that run on Make all which only validate F* files.
+ This allows validation time tests. If any validation fails, the file's tests fail.
+ 
+  Tests for an F* module FStar.M can be named Test.FStar.M.fst by default.
diff --git a/tests/validation-time/Test.FStar.String.fst b/tests/validation-time/Test.FStar.String.fst
new file mode 100644
index 00000000000..1e87cbb7278
--- /dev/null
+++ b/tests/validation-time/Test.FStar.String.fst
@@ -0,0 +1,89 @@
+module Test.FStar.String
+
+open FStar.String
+open FStar.Tactics.V2
+open FStar.IO
+
+
+open FStar.String
+open FStar.Class.Printable
+
+let _ = assert(streq "" "")
+let _ = assert(streq "A" "A")
+
+///   Is this caused by strlen being UTF8 characters instead of bytes?
+///  And there is no byte length.
+let _ = assert(strlen "A" = 1) by compute()
+let _ = assert(~(streq "A" "AB")) by compute()
+let _ = assert(streq_upto "A" "AB" 0)
+let _ = assert(streq_upto "AB" "AB" 0)
+
+[@@expect_failure]
+let _ = assert(streq_upto "AB" "AB" 1)
+
+let _ = assert(streq_upto "AB" "AB" 1) by compute()
+
+[@@expect_failure]
+let _ = assert(streq_upto "AB" "AB" 2)
+let _ = assert(streq_upto "AB" "AB" 2) by compute()
+
+[@@expect_failure]
+let _ = assert(~ (streq "A" "B"))
+let _ = assert(~(streq "A" "AB")) by compute()
+[@@expect_failure]
+let _ = assert(~(streq "AB" "Ab")) by compute()
+
+///  The boolean form is hidden behind the interface.
+[@@expect_failure]
+let _ = assert(~ (streq "A" "B")) by compute()
+let _ = assert(streq' "" "") by compute()
+[@@expect_failure]
+let _ = assert(not (streq' "" "A")) by compute()
+
+
+/// Of course by compute can't prove things it can't see a definition on.
+/// So once you hide it behind an interface it can't run it.
+/// So I need a test module but this goes in before Final so no tests yet.
+[@@expect_failure]
+let _ = assert(lines "" 0 = (0,0))  by compute()
+
+[@@expect_failure]
+let _ = assert(lines "A" 0 = (0,0)) by compute()
+let _ = assert(strlen "A" = 1)      by compute()
+
+let strlen_A_1 () : Lemma (strlen "A" = 1) = assert(strlen "A" = 1) by compute()
+[@@expect_failure]
+let _ = assert(strlen_A_1(); lines "A" 1 = (0,1)) by compute()
+
+[@@expect_failure]
+let _ = assert(strlen "A\n" = 2) by compute();
+        assert(lines "A\n" 1 = (0,1)) by compute()
+
+[@@expect_failure]
+let _ = assert(strlen "AB\nC\nD" = 6) by compute();
+        assert(lines  "AB\nC\nD" 0 = (0,0)) by compute()
+
+[@@expect_failure]
+let _ = assert(strlen "AB\nC\nD" = 6) by compute();
+        assert(lines  "AB\nC\nD" 1 = (0,1)) by compute()
+
+[@@expect_failure]
+let _ = assert(strlen "AB\nC\nD" = 6) by compute();
+        assert(lines  "AB\nC\nD" 2 = (0,2)) by compute()
+
+[@@expect_failure]
+let _ = assert(strlen "AB\nC\nD" = 6) by compute();
+        assert(lines  "AB\nC\nD" 3 = (1,0)) by compute()
+
+[@@expect_failure]
+let _ = assert(strlen "AB\nC\nD" = 6) by compute();
+        assert(lines  "AB\nC\nD" 4 = (1,1)) by compute()
+
+[@@expect_failure]
+let _ = assert(strlen "AB\nC\nD" = 6) by compute();
+        assert(lines  "AB\nC\nD" 5 = (2,0)) by compute()
+
+[@@expect_failure]
+let _ = assert(strlen "AB\nC\nD" = 6) by compute();
+        assert(lines  "AB\nC\nD" 6 = (2,1)) by compute()
+
diff --git a/tests/validation-time/Test.LexemeFL.fst b/tests/validation-time/Test.LexemeFL.fst
new file mode 100644
index 00000000000..9c2b311db43
--- /dev/null
+++ b/tests/validation-time/Test.LexemeFL.fst
@@ -0,0 +1,13 @@
+///  A new lexeme __FL__ has been added to show file and line (file(line)) to make writing tests easier.
+/// This file is line sensitive any edit will change the value of __FL__.
+module Test.LexemeFL
+open FStar.Tactics.V2
+open FStar.String
+module LT = FStar.List.Tot
+// Kinda funky to get a good validation time test, added Strings in other PR will fix this.
+// The lexer is sending back some strange character that we have to adjust.
+let fl = __FL__ 
+let _ = assert(fl <> "")
+let fl'  = string_of_list (list_of_string "Test.LexemFL.fst(11)")
+let _ = assert((strlen fl') = 20) by compute()
+let _ = assert(fl' = "Test.LexemFL.fst(11)") by compute()
diff --git a/ulib/FStar.String.Base.fst b/ulib/FStar.String.Base.fst
new file mode 100644
index 00000000000..7f6733cc6c7
--- /dev/null
+++ b/ulib/FStar.String.Base.fst
@@ -0,0 +1,77 @@
+(*
+   Copyright 2024 Microsoft Research
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.
+*)
+
+module FStar.String.Base
+
+open FStar.String
+
+let rec streq_upto' s1 (s2: string{strlen s1 = strlen s2})  (pos: nat{streq_upto s1 s2 pos}) :
+  Tot (b:bool{b <==> streq s1 s2})
+  (decreases strlen s1 - pos)
+=     
+ if pos = strlen s1 
+ then true
+ else if index s1 pos = index s2 pos
+ then streq_upto' s1 s2 (pos+1)
+ else false
+
+let streq' (s1 s2: string) : Tot (b:bool{b <==> streq s1 s2})
+=
+  if strlen s1 <> strlen s2
+  then false
+  else streq_upto' s1 s2 0 
+
+let rec first_diff' s1 s2
+   (pos: nat{pos <= strlen s1 /\ pos <= strlen s2 /\ streq_upto s1 s2 pos}) : 
+   Tot (o : (option (pos: nat{pos <= (min (strlen s1) (strlen s2))})) {
+             (None? o ==> strlen s1 = strlen s2 /\ streq_upto s1 s2 (strlen s1)) /\
+             (Some? o ==> 
+               streq_upto_min s1 s2 ((Some?.v o) - 1) /\
+              (((Some?.v o) = strlen s1  \/ (Some?.v o) = strlen s2) /\ strlen s1 <> strlen s2)
+              \/
+              (((Some?.v o) < strlen s1 /\ (Some?.v o) < strlen s2) /\
+                (index s1 (Some?.v o) <> (index s2 (Some?.v o)))))
+        })
+       (decreases (strlen s1 - pos))
+=
+ if pos = strlen s1 && pos = strlen s2
+ then None
+ else if pos >= (strlen s1) || pos >= (strlen s2)
+ then Some pos
+ else begin 
+   if (index s1 pos) <> (index s2 pos) 
+   then Some pos
+   else first_diff' s1 s2 (pos+1)
+ end
+
+let first_diff s1 s2 = first_diff' s1 s2 0
+
+let rec lines' s (upto:nat{upto <= strlen s}) 
+           lastnewline lines chars (pos: nat{pos <= upto && pos <= strlen s}) :
+  Tot (nat & nat) 
+      (decreases upto - pos)
+= if pos = upto 
+  then (if lastnewline then (lines+1, chars) else (lines, chars))
+  else if index s pos = '\n'  
+  then lines' s upto true  lines  0 (pos + 1)
+  else (if lastnewline 
+        then lines' s upto false (lines+1) chars    (pos + 1)
+        else lines' s upto false lines    (chars+1) (pos + 1))
+
+///  Return the line and character upto pos counting each starting at zero.
+let lines (s: string) (upto:nat{upto <= strlen s}) : Tot (nat & nat) = 
+  lines' s upto false 0 0 0
+  
diff --git a/ulib/FStar.String.Eq.fst b/ulib/FStar.String.Eq.fst
new file mode 100644
index 00000000000..0f2ab5c2efc
--- /dev/null
+++ b/ulib/FStar.String.Eq.fst
@@ -0,0 +1,49 @@
+(*
+   Copyright 2024 Microsoft Research
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.
+*)
+
+module FStar.String.Eq
+
+open FStar.List.Tot.Properties
+module EqRaw = FStar.Class.Eq.Raw
+module Eq  = FStar.Class.Eq
+
+open FStar.String
+open FStar.String.Base
+open FStar.String.Properties
+
+let decides_eqtype (#a:eqtype) (f : a -> a -> bool) : prop =
+  forall x y. f x y <==> x = y
+
+let streq'_decides_deq () :
+ Lemma (decides_eqtype streq')
+= introduce forall x y. streq' x y <==> x == y
+  with streq'_iff_eq x y
+
+instance streq'_is_deq : EqRaw.deq string = {
+  eq = streq'
+}
+
+///  Propeq properties 
+
+let streq'_decides_eq () :
+ Lemma (Eq.decides_eq streq')
+= introduce forall x y. streq' x y <==> x == y
+  with streq'_iff_propeq x y
+
+instance streq'_is_eq : Eq.deq string = {
+  raw    = streq'_is_deq;
+  eq_dec = streq'_decides_deq ()
+}
diff --git a/ulib/FStar.String.Properties.fst b/ulib/FStar.String.Properties.fst
new file mode 100644
index 00000000000..23dd41e517a
--- /dev/null
+++ b/ulib/FStar.String.Properties.fst
@@ -0,0 +1,233 @@
+(*
+   Copyright 2024 Microsoft Research
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.
+*)
+
+module FStar.String.Properties
+
+open FStar.String
+
+///  Length properties
+
+let strlen_is_list_length (s: string) :
+ Lemma (strlen s = List.Tot.length (list_of_string s))
+= ()
+
+let list_length_is_strlen (lc: list char) :
+ Lemma (strlen (string_of_list lc) = List.Tot.length lc)
+= list_of_string_of_list lc
+
+let streq_eq_lengths (s1 s2: string) :
+ Lemma (streq s1 s2 ==> strlen s1 = strlen s2)
+= ()
+
+let streq'_eq_lengths (s1 s2: string) :
+ Lemma (streq' s1 s2 ==> strlen s1 = strlen s2)
+= ()
+
+let strlen_string_of_char (c: char) :
+ Lemma ((strlen (string_of_char c)) = 1)
+= ()
+
+///  Index properties
+
+let indexes_eq_list_of_string (s:string)  :
+  Lemma (forall (i : nat{i < length s}). List.Tot.index (list_of_string s) i == index s i)
+= introduce forall (i : nat{i < length s}). List.Tot.index (list_of_string s) i == index s i
+  with index_list_of_string s i
+
+// Could be done with indexes_eq_list_of_string, but FStar.String does it with
+// list_of_string_of_list lc.
+let indexes_eq_string_of_list (lc: list char)  :
+  Lemma (list_of_string_of_list lc;
+         forall (i : nat{i < List.Tot.length lc}). 
+            index (string_of_list lc) i == List.Tot.index lc i)
+= list_of_string_of_list lc;
+  introduce forall (i : nat{i < List.Tot.length lc}). 
+             index (string_of_list lc) i == List.Tot.index lc i
+  with index_string_of_list lc i
+
+///  Relation Properties for streq
+
+let streq_refl (s: string) : 
+ Lemma (ensures  streq s s) 
+= ()
+
+let streq_sym (s1 s2: string) : 
+  Lemma (requires streq s1 s2) (ensures streq s2 s1)
+= ()
+
+let streq_trans (s1 s2 s3: string) :
+ Lemma (requires streq s1 s2 /\ streq s2 s3)
+       (ensures  streq s1 s2)
+= ()
+
+///  Streq_upto properties
+
+let streq_upto_strlen_impl_streq s1 s2 :
+  Lemma (requires streq_upto s1 s2 (strlen s1) /\ strlen s1 = strlen s2)
+        (ensures  streq s1 s2)
+= ()
+
+let streq_impl_streq_upto_strlen s1 s2 :
+  Lemma (requires  streq s1 s2)
+        (ensures streq_upto s1 s2 (strlen s1))
+= ()
+
+let streq_iff_streq_upto_strlen s1 s2 :
+  Lemma (requires strlen s1 = strlen s2)
+        (ensures streq s1 s2 <==> streq_upto s1 s2 (strlen s1))
+= 
+  assert(streq s1 s2 ==> streq_upto s1 s2 (strlen s1));
+  assert(streq_upto s1 s2 (strlen s1) ==> streq s1 s2)
+
+let streq_upto_zero s1 (s2: string{strlen s1 = strlen s2}) :
+  Lemma (streq_upto s1 s2 0)
+= ()
+
+///  Streq equivalance to streq'.
+
+let streq_impl_streq' s1 (s2: string{strlen s1 = strlen s2}) :
+ Lemma (streq s1 s2 ==> streq' s1 s2)
+= ()
+
+let streq'_impl_streq s1 (s2: string{strlen s1 = strlen s2}) :
+ Lemma (streq' s1 s2 ==> streq s1 s2)
+= ()
+
+let streq'_iff_streq s1 (s2: string{strlen s1 = strlen s2}) :
+ Lemma (streq' s1 s2 <==> streq s1 s2)
+= ()
+
+///  streq' equivalance to decideable equality.
+
+let streq'_impl_eq (s1 s2: string) :
+  Lemma (streq' s1 s2 ==> s1 = s2)
+= introduce streq' s1 s2 ==> s1 = s2
+  with pf_streq_s1_s2 .
+  begin
+   assert(strlen s1 = strlen s2);
+   assert(forall (i: nat{i < strlen s1}). index s1 i = index s2 i);
+   let l1 = (list_of_string s1) in
+   let l2 = (list_of_string s2) in
+     strlen_is_list_length s1;
+     strlen_is_list_length s2;
+     assert(List.length l1 == List.length l2);
+     indexes_eq_list_of_string s1;
+     indexes_eq_list_of_string s2;
+     assert(forall (i: nat) . i < List.length l1 ==> List.Tot.index l1 i == List.Tot.index l2 i);
+     List.Tot.index_extensionality l1 l2;
+     assert(l1 == l2);
+     string_of_list_of_string s1;
+     assert(string_of_list l1 == s1);
+     string_of_list_of_string s2;
+     assert(string_of_list l2 == s2)
+  end
+
+let eq_impl_streq' (s1 s2: string) :
+  Lemma (s1 = s2 ==> streq' s1 s2)
+= ()
+
+let streq'_iff_eq (s1 s2: string) :
+  Lemma (streq' s1 s2 <==> s1 = s2)
+= streq'_impl_eq s1 s2;
+  eq_impl_streq' s1 s2
+
+
+///  streq' equivalance to propositional equality.
+
+let streq'_impl_propeq (s1 s2: string) :
+  Lemma (streq' s1 s2 ==> s1 == s2)
+= streq'_impl_eq s1 s2
+
+let propeq_impl_streq' (s1 s2: string) :
+  Lemma (s1 == s2 ==> streq' s1 s2)
+= ()
+
+let streq'_iff_propeq (s1 s2: string) :
+  Lemma (streq' s1 s2 <==> s1 == s2)
+= streq'_impl_propeq s1 s2;
+  propeq_impl_streq' s1 s2
+
+///  streq equivalence to propositional equality.
+
+let streq_impl_propeq (s1 s2: string) :
+ Lemma (streq s1 s2 ==> s1 == s2)
+= streq'_impl_eq s1 s2
+
+let propeq_impl_streq (s1 s2: string) :
+ Lemma (s1 == s2 ==> streq s1 s2)
+= ()
+
+let streq_iff_propeq (s1 s2: string) :
+ Lemma (streq s1 s2 <==> s1 == s2)
+= streq_impl_propeq s1 s2;
+  propeq_impl_streq s1 s2
+
+///  streq equivalence to propositional equality.
+
+let streq_impl_deq (s1 s2: string) :
+ Lemma (streq s1 s2 ==> s1 = s2)
+= streq_impl_propeq s1 s2
+
+let deq_impl_streq (s1 s2: string) :
+ Lemma (s1 = s2 ==> streq s1 s2)
+= ()
+
+let streq_iff_deq (s1 s2: string) :
+ Lemma (streq s1 s2 <==> s1 = s2)
+= streq_impl_deq s1 s2;
+  deq_impl_streq s1 s2
+
+///  Empty string properties.
+
+let strlen_empty () :
+  Lemma (strlen "" = 0)
+= assert(strlen "" = 0) by FStar.Tactics.V2.compute()
+
+///  Difference Properties
+
+let first_diff'_none_strlen_same (s1 s2: string) :
+  Lemma (None? (first_diff' s1 s2 0) ==> strlen s1 = strlen s2)
+= ()
+
+let none_first_diff_impl_streq (s1 s2: string) :
+  Lemma (None? (first_diff s1 s2) ==> streq s1 s2)
+= ()
+
+let streq_impl_none_first_diff (s1 s2: string) :
+  Lemma (streq s1 s2 ==> None? (first_diff s1 s2))
+= ()
+
+let streq_iff_none_first_diff (s1 s2: string) :
+  Lemma (streq s1 s2 <==> None? (first_diff s1 s2))
+= none_first_diff_impl_streq s1 s2;
+  streq_impl_none_first_diff s1 s2
+
+let first_diff_strlen_neq (s1 s2 : string) :
+ Lemma (strlen s1 <> strlen s2 ==> Some? (first_diff s1 s2 ))
+= ()
+
+let first_diff_neq_some (s1 s2 : string) :
+ Lemma (s1 <> s2 ==> Some? (first_diff s1 s2))
+= if strlen s1 <> strlen s2 
+  then first_diff_strlen_neq s1 s2
+  else 
+    match first_diff s1 s2 with
+    | Some d -> ()
+    | None   -> begin 
+       none_first_diff_impl_streq s1 s2;
+       assert(streq s1 s2);
+       streq_impl_deq s1 s2
+     end 
diff --git a/ulib/FStar.String.fsti b/ulib/FStar.String.fsti
index ba6245670af..39009aa8b26 100644
--- a/ulib/FStar.String.fsti
+++ b/ulib/FStar.String.fsti
@@ -146,3 +146,50 @@ let concat_injective (s0 s0':string)
     string_of_list_of_string s0';
     string_of_list_of_string s1;
     string_of_list_of_string s1'
+
+///  Partial equivalence properties.
+let streq_upto s1 s2 (pos: nat) =
+  (pos <= strlen s1 /\ pos <= strlen s2 /\
+   (forall (i: nat{i < pos}). index s1 i = index s2 i))
+
+let streq_upto_min s1 s2 (pos: int{pos < (min (strlen s1) (strlen s2))}) =
+  (forall (i: nat{i < (pos - 1)}). index s1 i = index s2 i)
+
+///  The propositional form of streq.
+let streq (s1 s2: string) =
+  (strlen s1 = strlen s2 /\
+   (forall (i: nat{i < strlen s1}). index s1 i = index s2 i))
+
+///  The boolean form of streq.
+val streq_upto' s1 (s2: string{strlen s1 = strlen s2})  (pos: nat{streq_upto s1 s2 pos}) :
+  Tot (b:bool{b <==> streq s1 s2})
+
+val streq' (s1 s2: string) : Tot (b:bool{b <==> streq s1 s2})
+
+///  Return the first difference position upto a pos as an option.
+val first_diff' s1 s2
+   (pos: nat{pos <= strlen s1 /\ pos <= strlen s2 /\ streq_upto s1 s2 pos}) : 
+   Tot (o : (option (pos: nat{pos <= (min (strlen s1) (strlen s2))})) {
+             (None? o ==> strlen s1 = strlen s2 /\ streq_upto s1 s2 (strlen s1)) /\
+             (Some? o ==> 
+               streq_upto_min s1 s2 ((Some?.v o) - 1) /\
+              (((Some?.v o) = strlen s1  \/ (Some?.v o) = strlen s2) /\ strlen s1 <> strlen s2)
+              \/
+              (((Some?.v o) < strlen s1 /\ (Some?.v o) < strlen s2) /\
+                (index s1 (Some?.v o) <> (index s2 (Some?.v o)))))
+        })
+
+///  Return the first difference position as an option for the whole string.
+val first_diff (s1 s2: string) : 
+   Tot (o : (option (pos: nat{pos <= (min (strlen s1) (strlen s2))})) {
+             (None? o ==> strlen s1 = strlen s2 /\ streq_upto s1 s2 (strlen s1)) /\
+             (Some? o ==> 
+               streq_upto_min s1 s2 ((Some?.v o) - 1) /\
+              (((Some?.v o) = strlen s1  \/ (Some?.v o) = strlen s2) /\ strlen s1 <> strlen s2)
+              \/
+              (((Some?.v o) < strlen s1 /\ (Some?.v o) < strlen s2) /\
+                (index s1 (Some?.v o) <> (index s2 (Some?.v o)))))
+        })
+
+///  Return the line and character upto pos counting each starting at zero.
+val lines (s: string) (upto: nat{upto <= strlen s}) :  Tot (nat & nat) 
diff --git a/ulib/gmake/fstar.mk b/ulib/gmake/fstar.mk
index 71dc04ca735..9b39dd09e64 100644
--- a/ulib/gmake/fstar.mk
+++ b/ulib/gmake/fstar.mk
@@ -1,5 +1,5 @@
 HINTS_ENABLED?=--use_hints
-WARN_ERROR=
+WARN_ERROR?=
 OTHERFLAGS+=$(WARN_ERROR)
 
 ifdef Z3