put MiniSat back first -- Torlak's eval seemed to suggest that Crypto and Lingeling were better, but Crypto is slower on "Nitpick_Examples" and Crypto crashes
theory Realimports RComplete RealVectoruses "Tools/SMT/smt_real.ML"beginsetup {* SMT_Real.setup *}end