Right now, mk_smtlib2 and mk_smtlib2_single act and look very differently, and have very different types. mk_smtlib2 is only ever called inside Compare.mk_smtlib2_compare, where we compute a lot of values and information that should be computed inside mk_smtlib2. Moving this code will make mk_smtlib2 look much more like mk_smtlib2_single.
We should also rename mk_smtlib2 to mk_smtlib2_compare, or something similar.
Right now,
mk_smtlib2andmk_smtlib2_singleact and look very differently, and have very different types.mk_smtlib2is only ever called insideCompare.mk_smtlib2_compare, where we compute a lot of values and information that should be computed insidemk_smtlib2. Moving this code will makemk_smtlib2look much more likemk_smtlib2_single.We should also rename
mk_smtlib2tomk_smtlib2_compare, or something similar.