Fixed issue 823

[joe-hauns]

This PR fixes #823, and creates unit tests capturing the bug.

[mezpusz]

FOL regression over TPTP and ALASCA regression over TPTP+SMTLIB showed no change, except for the following benchmarks now timing out instead of crashing:

SMT-LIB/flat/AUFDTLIRA::20200306-Kanig::spark2014bench::NA29-017__prove_all__sorting.adb_90_44_overflow_check4___00.smt2
SMT-LIB/flat/AUFLIRA::nasa::fol_simplify_arithmetics::thruster_inuse_0105.fof.smt2
SMT-LIB/flat/AUFLIRA::nasa::fol_simplify_arithmetics::thruster_inuse_0106.fof.smt2
SMT-LIB/flat/AUFLIRA::nasa::fol_simplify_arithmetics::thruster_inuse_0107.fof.smt2
SMT-LIB/flat/AUFLIRA::nasa::fol_simplify_structure_forall::quaternion_ds1_inuse_0002.fof.smt2
SMT-LIB/flat/AUFLIRA::nasa::fol_simplify_structure_forall::quaternion_ds1_inuse_0003.fof.smt2
SMT-LIB/flat/AUFLIRA::nasa::fol_simplify_structure_prop::quaternion_ds1_inuse_0002.fof.smt2
SMT-LIB/flat/AUFLIRA::nasa::fol_simplify_structure_prop::quaternion_ds1_inuse_0003.fof.smt2
SMT-LIB/flat/AUFLIRA::nasa::fol_simplify_structure_prop::thruster_inuse_0102.fof.smt2
SMT-LIB/flat/AUFLIRA::nasa::fol_simplify_structure_prop::thruster_inuse_0103.fof.smt2
SMT-LIB/flat/AUFLIRA::nasa::fol_simplify_structure_prop::thruster_inuse_0104.fof.smt2
SMT-LIB/flat/AUFLIRA::nasa::vc_normalize_subst::quaternion_ds1_inuse_0001.fof.smt2