FStar
FStar copied to clipboard
minor adjustment to `new_z3proc_with_id`
This function was failing in my environment and it seems to fix it.
This is checking just the prefix of the output rather than the whole of it.
Context: I was running Verify current file in the command line in emacs
before:
"C:/dev/src/github.com/FStar/FStar/bin/fstar.exe" "c:/dev/src/github.com/mateuszbujalski/jsonstar/jsonstar/JsonStar.Json.fst" "--smt" "C:/dev/bin/z3-4.8.5-x64-win/bin/z3.exe" Unexpected error; please file a bug report, ideally with a minimized version of the source program that triggered the error. Failed to start and test Z3 process, expected output "Test" got "Test Done! "
after:
"C:/dev/src/github.com/FStar/FStar/bin/fstar.exe" "c:/dev/src/github.com/mateuszbujalski/jsonstar/jsonstar/JsonStar.Json.fst" "--smt" "C:/dev/bin/z3-4.8.5-x64-win/bin/z3.exe" C:\dev\src\github.com\FStar\FStar\ulib\prims.fst(0,0-0,0): (Warning 241) Unable to load C:\dev\src\github.com\FStar\FStar\ulib\prims.fst.checked since checked file C:\dev\src\github.com\FStar\FStar\ulib\prims.fst.checked does not exist; will recheck C:\dev\src\github.com\FStar\FStar\ulib\prims.fst (suppressing this warning for further modules) Verified module: JsonStar.Json All verification conditions discharged successfully
Please let me know any of the adjustments you'd like, or if there is an approach you'd like me to take to add a test.
Hi @smoothdeveloper, thanks for submitting this PR. I looked into it a little. I am curious to know why is there an error on your configuration, while all of us use it without any problems. In particular, the "Done!" part should not be returned to this function that you are modifying.
Do you have any insights on this?