[isabelle-dev] status of remote_z3

[Makarius]

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