What is the status of remote_z3?
Doing some routine maintenance (e.g. cb9d981fa9a0), I've come across it,
and tried it out to see if it still works. All I managed was to produce
the following example error:
declare [[smt_solver = remote_z3, smt_trace]]
lemma "(p1 ∧ p2) ∨ p3 ⟶ (p1 ⟶ (p3 ∧ p2) ∨ (p1 ∧ p3)) ∨ p1" by smt
...
SMT: Result:
ssh: connect to host lxlabbroy11 port 22: No route to host
What is the purpose of remote_z3 anyway? Doesn't it require the same
non-commercial user agreement as the local version? Maybe it is just a
left-over from the old times where Z3 was not uniformly available on all
platforms, and we didn't have an Isabelle component for it.
Makarius_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
