diff options
| author | Quentin Garchery <garchery.quentin@gmail.com> | 2018-10-27 20:08:44 +0200 |
|---|---|---|
| committer | Valentin Blot <24938579+vblot@users.noreply.github.com> | 2018-10-28 00:39:25 +0200 |
| commit | faaa2848c37444f8f37ac432c25f9f813e1df39b (patch) | |
| tree | 2672d165fd13b5262005406d1496bc6a14e8b521 /src/zchaff/satParser.ml | |
| parent | 7940ef63c654be26b41ce20162207f3c67d0b10a (diff) | |
| download | smtcoq-faaa2848c37444f8f37ac432c25f9f813e1df39b.tar.gz smtcoq-faaa2848c37444f8f37ac432c25f9f813e1df39b.zip | |
Adding support for lemmas in the command verit
Diffstat (limited to 'src/zchaff/satParser.ml')
| -rw-r--r-- | src/zchaff/satParser.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/zchaff/satParser.ml b/src/zchaff/satParser.ml index 79d0b14..9e624ed 100644 --- a/src/zchaff/satParser.ml +++ b/src/zchaff/satParser.ml @@ -26,7 +26,7 @@ let buff_length = 1024 let open_file s name = try let in_channel = open_in name in - let buff = String.create buff_length in + let buff = Bytes.create buff_length in let buff_end = input in_channel buff 0 buff_length in { buff = buff; curr_char = 0; buff_end = buff_end; in_ch = in_channel } with _ -> @@ -83,7 +83,7 @@ let skip_string lb s = let match_string lb s = if not (skip_string lb s) then raise (Invalid_argument ("match_string "^s)) -let aux_buff = String.create buff_length +let aux_buff = Bytes.create buff_length let aux_be = ref 0 let aux_pi = ref 0 let aux_cc = ref 0 |