[isabelle] Z3 on a Mac



Hello,

Has anyone used Z3 (with the smt method) on a Mac? 

I've set the Z3_NON_COMMERCIAL variable to "yes", but the smt method fails 
(with a "Failed to finish proof" message).

Note that the smt method works fine with cvc3 (when I set "declare [[ smt_solver = cvc3 ]]").

Thanks,

Gudmund
-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.