[isabelle-dev] status of remote_z3
makarius at sketis.net
Mon Jan 6 18:28:14 CET 2014
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
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.
More information about the isabelle-dev