Adapt z3 constraint checking logic to windows

[wanghuibin0]

On Windows, the output of z3 has a trailing \r, which makes checking of "result = 'unsat'" return false.
Checking the prefix of the output is enough and it adapts to different types of OS.

[wanghuibin0]

Could you help review this PR? @Alasdair

[Alasdair]

I think a problem with this is z3 often produces output like:

unsat
(error <message>)

so it's actually unsafe to just check the prefix

[Alasdair]

Although the output is split by lines, so maybe that's not really a problem.

However, reading the code more closely I think the problem is really that input_line doesn't do the right thing for \r\n line endings. In OCaml the situation is a bit weird because some stdlib channel functions will attempt to automatically normalise line endings to just '\n' (which you often don't want, and use open_in_bin to avoid), and the stdlib functions that work on strings just assume a plain \n. I am sure there are issues all over the place where we aren't doing the right thing for \r\n endings.

[github-actions]

Test Results

   13 files  ±0     29 suites  ±0   0s ⏱️ ±0s
  841 tests ±0    841 ✅ ±0  0 💤 ±0  0 ❌ ±0 
3 516 runs  ±0  3 516 ✅ ±0  0 💤 ±0  0 ❌ ±0 

Results for commit 0b63afd. ± Comparison against base commit fbdcb92.

[wanghuibin0]

Ah, at present I discovered only this issue when I run sail on Windows.
Do you have any idea where other similar issues are?