Add OptionException handling during initialization (#2466)

The initial motivation for this commit was that dump with an invalid tag
was leading to a segfault. The reason for the segfault was as follows:

1. `api::Solver` creates an `ExprManager`, which is stored in a
`unique_ptr` as a class member
2. The `api::Solver` tries to create an SmtEngine instance
3. The `SmtEnginePrivate` constructor subscribes to events in the
NodeManager and starts registering option listeners
4. When the `SmtEnginePrivate` gets to registerSetDumpModeListener, it
registers and notifies the DumpModeListener which calls
Dump::setDumpFromString, which fails with an `OptionException` due to
the invalid tag
5. While propagating the exception through `api::Solver`, the
`ExprManager` is deleted but the non-existent `SmtEnginePrivate` is
still subscribed to its events and there are still option listeners
registered. This leads to a segfault because the NodeManager tries to
notify the `SmtEnginePrivate` about deleted nodes

This commit fixes the issue by catching the `OptionException` in
`SmtEnginePrivate`, unsubscribing the `SmtEnginePrivate` from the
NodeManager events and deleting its option listener registrations before
rethrowing the exception. In addition, it changes the
`Options::registerAndNotify()` method to immediately delete a
registration if notifying the registration resulted in an
``OptionException`` (otherwise only the `ListenerCollection` knows about
the registration and complains about it in its destructor).  Finally,
the commit adds a simple regression test for invalid dump tags.

3 files changed, 22 insertions, 16 deletions

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 5d0459015..e489d2e21 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -155,6 +155,8 @@ set(regress_0_tests
   regress0/bug605.cvc
   regress0/bug639.smt2
   regress0/buggy-ite.smt2
+  regress0/bv/ackermann1.smt2
+  regress0/bv/ackermann2.smt2
   regress0/bv/bool-to-bv.smt2
   regress0/bv/bug260a.smt
   regress0/bv/bug260b.smt
@@ -340,6 +342,7 @@ set(regress_0_tests
   regress0/datatypes/cdt-non-canon-stream.smt2
   regress0/datatypes/coda_simp_model.smt2
   regress0/datatypes/conqueue-dt-enum-iloop.smt2
+  regress0/datatypes/data-nested-codata.smt2
   regress0/datatypes/datatype.cvc
   regress0/datatypes/datatype0.cvc
   regress0/datatypes/datatype1.cvc
@@ -434,8 +437,10 @@ set(regress_0_tests
   regress0/fmf/quant_real_univ.cvc
   regress0/fmf/sat-logic.smt2
   regress0/fmf/sc_bad_model_1221.smt2
+  regress0/fmf/sort-infer-typed-082718.smt2
   regress0/fmf/syn002-si-real-int.smt2
   regress0/fmf/tail_rec.smt2
+  regress0/fp/ext-rew-test.smt2
   regress0/fp/simple.smt2
   regress0/fuzz_1.smt
   regress0/fuzz_3.smt
@@ -496,9 +501,11 @@ set(regress_0_tests
   regress0/logops.05.cvc
   regress0/model-core.smt2
   regress0/nl/coeff-sat.smt2
+  regress0/nl/ext-rew-aggr-test.smt2
   regress0/nl/magnitude-wrong-1020-m.smt2
   regress0/nl/mult-po.smt2
   regress0/nl/nia-wrong-tl.smt2
+  regress0/nl/nlExtPurify-test.smt2
   regress0/nl/nta/cos-sig-value.smt2
   regress0/nl/nta/exp-n0.5-lb.smt2
   regress0/nl/nta/exp-n0.5-ub.smt2
@@ -512,6 +519,7 @@ set(regress_0_tests
   regress0/nl/subs0-unsat-confirm.smt2
   regress0/nl/very-easy-sat.smt2
   regress0/nl/very-simple-unsat.smt2
+  regress0/options/invalid_dump.smt2
   regress0/parallel-let.smt2
   regress0/parser/as.smt2
   regress0/parser/constraint.smt2
@@ -616,6 +624,7 @@ set(regress_0_tests
   regress0/quantifiers/issue1805.smt2
   regress0/quantifiers/issue2031-bv-var-elim.smt2
   regress0/quantifiers/issue2033-macro-arith.smt2
+  regress0/quantifiers/issue2035.smt2
   regress0/quantifiers/lra-triv-gn.smt2
   regress0/quantifiers/macros-int-real.smt2
   regress0/quantifiers/macros-real-arg.smt2
@@ -791,6 +800,7 @@ set(regress_0_tests
   regress0/simplification_bug2.smt
   regress0/smallcnf.cvc
   regress0/smt2output.smt2
+  regress0/smtlib/get-unsat-assumptions.smt2
   regress0/strings/bug001.smt2
   regress0/strings/bug002.smt2
   regress0/strings/bug612.smt2
@@ -811,12 +821,14 @@ set(regress_0_tests
   regress0/strings/norn-31.smt2
   regress0/strings/norn-simp-rew.smt2
   regress0/strings/repl-rewrites2.smt2
+  regress0/strings/rewrites-re-concat.smt2
   regress0/strings/rewrites-v2.smt2
   regress0/strings/std2.6.1.smt2
   regress0/strings/stoi-solve.smt2
   regress0/strings/str003.smt2
   regress0/strings/str004.smt2
   regress0/strings/str005.smt2
+  regress0/strings/str_unsound_ext_rew_eq.smt2
   regress0/strings/strings-charat.cvc
   regress0/strings/strings-native-simple.cvc
   regress0/strings/strip-endpoint-itos.smt2
@@ -830,6 +842,7 @@ set(regress_0_tests
   regress0/sygus/check-generic-red.sy
   regress0/sygus/const-var-test.sy
   regress0/sygus/dt-no-syntax.sy
+  regress0/sygus/hd-05-d1-prog-nogrammar.sy
   regress0/sygus/inv-different-var-order.sy
   regress0/sygus/let-ringer.sy
   regress0/sygus/let-simp.sy
@@ -1000,18 +1013,6 @@ set(regress_0_tests
   regress0/wiki.19.cvc
   regress0/wiki.20.cvc
   regress0/wiki.21.cvc
-  regress0/bv/ackermann1.smt2
-  regress0/bv/ackermann2.smt2
-  regress0/datatypes/data-nested-codata.smt2
-  regress0/fmf/sort-infer-typed-082718.smt2
-  regress0/fp/ext-rew-test.smt2
-  regress0/nl/ext-rew-aggr-test.smt2
-  regress0/nl/nlExtPurify-test.smt2
-  regress0/quantifiers/issue2035.smt2
-  regress0/smtlib/get-unsat-assumptions.smt2
-  regress0/strings/rewrites-re-concat.smt2
-  regress0/strings/str_unsound_ext_rew_eq.smt2
-  regress0/sygus/hd-05-d1-prog-nogrammar.sy
 )
 
 #-----------------------------------------------------------------------------#
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 194a4ddaf..5b2280b02 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -10,12 +10,12 @@ REG0_TESTS = \
 	regress0/arith/bug547.2.smt2 \
 	regress0/arith/bug569.smt2 \
 	regress0/arith/delta-minimized-row-vector-bug.smt \
+	regress0/arith/div-chainable.smt2 \
 	regress0/arith/div.01.smt2 \
 	regress0/arith/div.02.smt2 \
 	regress0/arith/div.04.smt2 \
 	regress0/arith/div.05.smt2 \
 	regress0/arith/div.07.smt2 \
-	regress0/arith/div-chainable.smt2 \
 	regress0/arith/fuzz_3-eq.smt \
 	regress0/arith/integers/arith-int-042.cvc \
 	regress0/arith/integers/arith-int-042.min.cvc \
@@ -343,6 +343,7 @@ REG0_TESTS = \
 	regress0/datatypes/cdt-non-canon-stream.smt2 \
 	regress0/datatypes/coda_simp_model.smt2 \
 	regress0/datatypes/conqueue-dt-enum-iloop.smt2 \
+	regress0/datatypes/data-nested-codata.smt2 \
 	regress0/datatypes/datatype.cvc \
 	regress0/datatypes/datatype0.cvc \
 	regress0/datatypes/datatype1.cvc \
@@ -350,7 +351,6 @@ REG0_TESTS = \
 	regress0/datatypes/datatype2.cvc \
 	regress0/datatypes/datatype3.cvc \
 	regress0/datatypes/datatype4.cvc \
-	regress0/datatypes/data-nested-codata.smt2 \
 	regress0/datatypes/dt-2.6.smt2 \
 	regress0/datatypes/dt-match-pat-param-2.6.smt2 \
 	regress0/datatypes/dt-param-2.6.smt2 \
@@ -441,8 +441,8 @@ REG0_TESTS = \
 	regress0/fmf/sort-infer-typed-082718.smt2 \
 	regress0/fmf/syn002-si-real-int.smt2 \
 	regress0/fmf/tail_rec.smt2 \
-	regress0/fp/simple.smt2 \
 	regress0/fp/ext-rew-test.smt2 \
+	regress0/fp/simple.smt2 \
 	regress0/fuzz_1.smt \
 	regress0/fuzz_3.smt \
 	regress0/get-value-incremental.smt2 \
@@ -520,6 +520,7 @@ REG0_TESTS = \
 	regress0/nl/subs0-unsat-confirm.smt2 \
 	regress0/nl/very-easy-sat.smt2 \
 	regress0/nl/very-simple-unsat.smt2 \
+	regress0/options/invalid_dump.smt2 \
 	regress0/parallel-let.smt2 \
 	regress0/parser/as.smt2 \
 	regress0/parser/constraint.smt2 \
@@ -827,10 +828,10 @@ REG0_TESTS = \
 	regress0/strings/str003.smt2 \
 	regress0/strings/str004.smt2 \
 	regress0/strings/str005.smt2 \
+	regress0/strings/str_unsound_ext_rew_eq.smt2 \
 	regress0/strings/strings-charat.cvc \
 	regress0/strings/strings-native-simple.cvc \
 	regress0/strings/strip-endpoint-itos.smt2 \
-	regress0/strings/str_unsound_ext_rew_eq.smt2 \
 	regress0/strings/substr-rewrites.smt2 \
 	regress0/strings/type001.smt2 \
 	regress0/strings/unsound-0908.smt2 \
diff --git a/test/regress/regress0/options/invalid_dump.smt2 b/test/regress/regress0/options/invalid_dump.smt2
new file mode 100644
index 000000000..9f92a7a64
--- /dev/null
+++ b/test/regress/regress0/options/invalid_dump.smt2
@@ -0,0 +1,4 @@
+; COMMAND-LINE: --dump invalidDumpTag
+; ERROR-SCRUBBER: grep -o "unknown option for --dump"
+; EXPECT-ERROR: unknown option for --dump
+; EXIT: 1