[Consolidated] soundness issues, invalid models, and crashes for options "tactic.default_tactic=smt sat.euf=true" (2)

[zhendongsu]

Commit: ba56bfa
OS: Ubuntu 18.04

Refutation unsoundness:

[526] % z3release small.smt2
sat
[527] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
unsat
[528] % cat small.smt2
(declare-const a Real)
(assert (not (< (* a a) 0 0)))
(check-sat)
[529] % 

[zhendongsu]

[516] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
ASSERTION VIOLATION
File: ../src/sat/smt/euf_internalize.cpp
Line: 278
Failed to verify: v != sat::null_bool_var

Z3 4.8.11.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new
[517] % z3debug tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
ASSERTION VIOLATION
File: ../src/sat/smt/q_mam.cpp
Line: 3777
t->has_candidates()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[518] % 
[518] % cat small.smt2
(declare-datatypes ((a 0)) (((b (c a) (k a)) (d (l a)) (m (e a) (f a)) (g))))
(declare-fun h () a)
(declare-fun i (a) a)
(assert
 (forall ((j a))
  (= (m j j)
   (ite (and ((_ is b) j))
    (m (i (d (c (l j)))) (i (d (k j))))
    (ite (and ((_ is m) j))
     (b (i (d (e (l j)))) (i (d (f (l j)))))
     (ite (and ((_ is d) j))
      (i (l (l j))) h))))))
(check-sat)
[519] % 

[zhendongsu]

Solution unsoundness:

[507] % z3release small.smt2
unsat
[508] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
sat
[509] % cat small.smt2
(declare-fun a () Real)
(assert (forall ((b Real)) (and (= a b) (= 0 0))))
(check-sat)
[510] % 

[zhendongsu]

[528] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
Segmentation fault
[529] % z3debug tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
ASSERTION VIOLATION
File: ../src/sat/smt/euf_model.cpp
Line: 214
Failed to verify: arg

[530] % z3san tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
ASAN:DEADLYSIGNAL
=================================================================
==20408==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000004 (pc 0x55bbd7e5036e bp 0x7ffc5fa43fd0 sp 0x7ffc5fa43ef0 T0)
==20408==The signal is caused by a READ memory access.
==20408==Hint: address points to the zero page.
    #0 0x55bbd7e5036d in ast::get_kind() const ../src/ast/ast.h:501
    #1 0x55bbd7e5036d in is_app(ast const*) ../src/ast/ast.h:914
    #2 0x55bbd7e5036d in ast_manager::are_equal(expr*, expr*) const ../src/ast/ast.cpp:1643
    #3 0x55bbd6b7bb62 in func_entry::eq_args(ast_manager&, unsigned int, expr* const*) const ../src/model/func_interp.cpp:57
    #4 0x55bbd6b7bb62 in func_interp::get_entry(expr* const*) const ../src/model/func_interp.cpp:180
    #5 0x55bbd5c090db in euf::solver::values2model(top_sort<euf::enode> const&, ref<model>&) ../src/sat/smt/euf_model.cpp:216
    #6 0x55bbd5c10edb in euf::solver::update_model(ref<model>&) ../src/sat/smt/euf_model.cpp:73
    #7 0x55bbd5b88e67 in sat_tactic::imp::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/sat/tactic/sat_tactic.cpp:109
    #8 0x55bbd5b8b105 in sat_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/sat/tactic/sat_tactic.cpp:202
    #9 0x55bbd6a9c4f8 in cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:924
    #10 0x55bbd6a670de in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:150
    #11 0x55bbd6a68a87 in check_sat(tactic&, ref<goal>&, ref<model>&, labels_vec&, obj_ref<app, ast_manager>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >&) ../src/tactic/tactic.cpp:170
    #12 0x55bbd68b22f0 in check_sat_core2 ../src/solver/tactic2solver.cpp:187
    #13 0x55bbd68d58ef in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
    #14 0x55bbd68ee334 in combined_solver::check_sat_core(unsigned int, expr* const*) ../src/solver/combined_solver.cpp:252
    #15 0x55bbd68c32a6 in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:332
    #16 0x55bbd683d8c5 in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1647
    #17 0x55bbd679ad93 in smt2::parser::parse_check_sat() ../src/parsers/smt2/smt2parser.cpp:2607
    #18 0x55bbd679ad93 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2949
    #19 0x55bbd679ad93 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3141
    #20 0x55bbd674ff75 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3190
    #21 0x55bbd3ab04ff in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:142
    #22 0x55bbd3a5ae24 in main ../src/shell/main.cpp:371
    #23 0x7f842b2a4b96 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21b96)
    #24 0x55bbd3a70c79 in _start (/local/suz-local/software/z3san/build-05312021190355-ba56bfa/z3+0x208c79)

AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV ../src/ast/ast.h:501 in ast::get_kind() const
==20408==ABORTING
[531] % 
[531] % cat small.smt2
(set-option :smt.arith.reflect false)
(declare-const x Real)
(assert (= 0 (* (/ 0 0) (/ 0 (- 1.0) (* x x)))))
(check-sat)
[532] % 

[zhendongsu]

Invalid model:

[518] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
sat
(error "line 6 column 10: an invalid model was generated")
(
  (define-fun a () Real
    0.0)
  (define-fun b () Bool
    false)
  (define-fun c () Bool
    false)
)
[519] % cat small.smt2
(declare-const a Real)
(declare-const b Bool)
(declare-const c Bool)
(assert (or b c))
(maximize a)
(check-sat)
(get-model)
[520] % 

[rainoftime]

Refutation soundness

(declare-const x Bool)
(assert (exists ((s Real)) (or x (not x))))
(check-sat)

 z3 xx.smt2
sat
z3 tactic.default_tactic=smt sat.euf=true xx.smt2
unsat

[rainoftime]

Invalid model

(declare-fun y () Int)
(declare-fun x () Int)
(assert (and (= 1 y) (< 1 x)))
(check-sat-using (then dom-simplify add-bounds normalize-bounds smt))

z3 tactic.default_tactic=smt sat.euf=true model_validate=true delta.out.smt2
sat
(error "line 4 column 68: an invalid model was generated")

[rainoftime]

src/ast/ast.h:934

(assert (exists ((T2_673 (_ BitVec 1))) (forall ((T1_734 (_ BitVec 1))) (let (($x31 true))))))
(check-sat)


z3 tactic.default_tactic=smt sat.euf=true delta.out.smt2
ASSERTION VIOLATION
File: ../src/ast/ast.h
Line: 934
is_quantifier(n)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[rainoftime]

heap-use-after-free

(declare-fun A (Int) Bool)
(declare-fun B (Int) Bool)
(declare-fun C (Int) Bool)
(declare-fun D (Int) Bool)
(assert (forall ((x Int)) (=> (or (A x) (B x)) (D x))))
(assert (forall ((x Int)) (iff (D x) (C x))))
(assert (B 1))
(check-sat)

READ of size 8 at 0x603000018b38 thread T0
    #0 0x247d2f8 in q::mam_impl::propagate() /home/z3-debug/build/../src/sat/smt/q_mam.cpp:3776:31
    #1 0x23ef98d in q::ematch::propagate(bool) /home/z3-debug/build/../src/sat/smt/q_ematch.cpp:468:16
    #2 0x234f280 in q::solver::unit_propagate() /home//z3-debug/build/../src/sat/smt/q_solver.cpp:95:57
    #3 0x22521f5 in euf::solver::unit_propagate() /home//z3-debug/build/../src/sat/smt/euf_solver.cpp:336:24

[rainoftime]

src/sat/smt/arith_solver.cpp:833

(declare-fun rr1 () Real)
(assert (let (($x437 (and (= 0.0 (- rr1 rr1)) (not (= rr1 0.0)))))))
(check-sat)

z3 tactic.default_tactic=smt sat.euf=true delta.out.smt2
ASSERTION VIOLATION
File: ../src/sat/smt/arith_solver.cpp
Line: 833
is_registered_var(v)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[rainoftime]

src/sat/smt/q_mam.cpp:2257

(declare-fun q (Int) Bool)
(assert (forall ((x Int)) (forall ((z Int)) (or (q z) (= z 1)))))
(check-sat)
(check-sat-using qffd)

z3 tactic.default_tactic=smt sat.euf=true delta.out.smt2
sat
ASSERTION VIOLATION
File: ../src/sat/smt/q_mam.cpp
Line: 2257
ctx.is_relevant(n)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[rainoftime]

src/util/vector.h:474

(assert (forall ((z2 (_ BitVec 1))) (exists ((x (_ BitVec 2))) (= x (_ bv1 2)))))
(check-sat)

z3 tactic.default_tactic=smt sat.euf=true delta.out.smt2
ASSERTION VIOLATION
File: ../src/util/vector.h
Line: 474
idx < size()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[rainoftime]

src/sat/smt/arith_solver.cpp:584

(set-option :rewriter.mul_to_power true)
(declare-fun x2 () Int)
(assert (and (< x2 1) (< x2 (- 1))))
(check-sat)

ASSERTION VIOLATION
File: ../src/sat/smt/arith_solver.cpp
Line: 584
UNEXPECTED CODE WAS REACHED.
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[rainoftime]

src/sat/smt/array_solver.cpp:194

(declare-fun f () (Set Int))
(assert (= f (complement f)))
(check-sat-using bv)

z3 tactic.default_tactic=smt sat.euf=true delta.out.smt2
ASSERTION VIOLATION
File: ../src/sat/smt/array_solver.cpp
Line: 194
can_beta_reduce(lambda)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[rainoftime]

src/util/sat_literal.h:48

(declare-fun q (Int) Bool)
(declare-fun bb8 () Bool)
(declare-fun l3 () Bool)
(assert (let (($x6 (q 0)))))
(assert (= l3 (forall ((x1 Int)) (not (q x1)))))
(assert (= l3 (and bb8)))
(check-sat)

z3 tactic.default_tactic=smt sat.euf=true xx.smt2
ASSERTION VIOLATION
File: ../src/util/sat_literal.h
Line: 48
var() == v
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[zhendongsu]

Adding a few more tests:

[578] % z3debug tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
ASSERTION VIOLATION
File: ../src/math/simplex/model_based_opt.cpp
Line: 185
index == 0 || r.m_type != t_mod || (mod(r.m_value, r.m_mod).is_zero())
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[579] % cat small.smt2
(set-option :smt.ematching false)
(declare-sort a)
(declare-fun b (Int) a)
(assert (forall ((c Int)) (not (= (b (* 3 c)) (b 1)))))
(check-sat)
[580] % 

[zhendongsu]

[567] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
ASSERTION VIOLATION
File: ../src/sat/smt/q_eval.cpp
Line: 263
UNEXPECTED CODE WAS REACHED.
Z3 4.8.11.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new
[568] % z3debug tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
ASSERTION VIOLATION
File: ../src/sat/smt/q_eval.cpp
Line: 242
l_false == compare(n, binding, s, t)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[569] % cat small.smt2
(declare-fun a (Int Int) Int)
(declare-fun b (Int Int Real) (Array Int (Array Int Real)))
(assert (forall ((c Int) (d Int) (j Int) (e Int) (f Int) (k Int) (l Real)) (=> (=> true (<= e k)) (= (select (select (b (a d j) (a f k) l) c) e) l))))
(assert (forall ((g Int) (h Int) (i (Array Int (Array Int Real)))) (and (distinct (select (i g) h) (select (i h) g)) (= 0 0))))
(check-sat)
[570] % 

[zhendongsu]

[546] % z3debug tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
Failed to validate 1 30: #30 false
ASSERTION VIOLATION
File: ../src/util/vector.h
Line: 479
idx < size()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[547] % cat small.smt2
(set-option :smt.arith.reflect false)
(declare-fun a () Int)
(declare-fun b () (Array Int Real))
(assert (forall ((c (Array Int Int))) (not (< 0 (select b a)))))
(check-sat)
[548] % 

[zhendongsu]

[543] % z3debug tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
ASSERTION VIOLATION
File: ../src/qe/mbp/mbp_arith.cpp
Line: 73
m.limit().is_canceled() || !m.is_false(val)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[544] % cat small.smt2
(declare-fun dim (Int Int) Int)
(declare-fun a (Int Real) (Array Int Real))
(assert (forall ((b Int) (c Int) (e Int) (d Real)) (=> (<= c b e) (= (select (a (dim c e) d) b) d))))
(check-sat)
[545] % 

[zhendongsu]

[542] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
ASSERTION VIOLATION
File: ../src/sat/smt/q_solver.h
Line: 77
UNEXPECTED CODE WAS REACHED.
Z3 4.8.11.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new
[543] % cat small.smt2
(declare-sort a)
(declare-sort b)
(declare-sort c)
(declare-sort d)
(declare-sort s)
(declare-sort e)
(declare-sort f)
(declare-sort g)
(declare-fun h () a)
(declare-fun i (c b) a)
(declare-fun j () c)
(declare-fun k (s e) a)
(declare-fun l (b d) s)
(declare-fun m (f) e)
(declare-fun n (g) f)
(declare-fun o () g)
(assert
 (forall ((p b))
  (distinct (distinct (i j p) h)
   (exists ((q d) (r b)) (distinct (k (l r q) (m (n o))) h)))))
(check-sat)
[544] % 

[zhendongsu]

[547] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
Segmentation fault
[548] % z3debug tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
ASSERTION VIOLATION
File: ../src/ast/rewriter/bv_rewriter.cpp
Line: 90
num_args > 0
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[549] % cat small.smt2
(set-option :smt.bv.reflect false)
(declare-fun a () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun b () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun c () (_ BitVec 32))
(assert (= b (store (store (store (store a (bvadd (_ bv3 32))
  ((_ extract 7 0) (bvlshr c (_ bv24 32)))) (bvudiv (_ bv134567808 32)
  (_ bv2 32)) ((_ extract 7 0) (bvlshr c (_ bv16 32))))
  (bvmul (_ bv134567808 32) (_ bv1 32)) ((_ extract 7 0) (bvlshr c (_ bv8 32))))
  (bvadd (_ bv0 32)) ((_ extract 7 0) c))))
(check-sat)
[550] % 

[zhendongsu]

Possibly related: #5324 (comment), but the release build doesn't segfault on that instance.

[581] % z3release tactic.default_tactic=smt sat.euf=true small.smt2
Segmentation fault
[582] % z3debug tactic.default_tactic=smt sat.euf=true small.smt2
ASSERTION VIOLATION
File: ../src/util/vector.h
Line: 474
idx < size()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[583] % cat small.smt2
(declare-datatypes ((c 0)) (((a (g (_ BitVec 32)) (d c)) h)))
(declare-fun e () Bool)
(declare-fun b (c (_ BitVec 32)) Bool)
(assert (forall ((f c) (i (_ BitVec 32))) (distinct (or (or (= (g f) i)) (b (d f) i)) e)))
(check-sat)
[584] % 

[zhendongsu]

Invalid model (for a and b of other types, valid models are returned):

[536] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2 
sat
(error "line 4 column 10: an invalid model was generated")
(
  (define-fun a () String
    "")
  (define-fun b () String
    "")
)
[537] % cat small.smt2 
(declare-fun a () String)
(declare-fun b () String)
(assert (not (= a b)))
(check-sat)
(get-model)
[538] % 

[zhendongsu]

Invalid model:

[574] % z3release model_validate=true tactic.default_tactic=smt sat.euf=true small.smt2
Failed to validate 3 43: (= (a 4) 0) false
41: (a 4)
(- 5)
42: 0
0
sat
(error "line 7 column 10: an invalid model was generated")
(
  (define-fun b () Int
    0)
  (define-fun c () Int
    (- 5))
  (define-fun a ((x!1 Int)) Int
    (ite (= x!1 4) (- 5)
      #unspecified))
)
[575] % cat small.smt2
(declare-fun a (Int) Int)
(declare-fun b () Int)
(declare-fun c () Int)
(assert (< c (- 4)))
(assert (= c (* (a (- 4 b)))))
(assert (= (a 4) 0))
(check-sat)
(get-model)
[576] % 

[zhendongsu]

Invalid model:

[591] % z3release model_validate=true tactic.default_tactic=smt sat.euf=true small.smt2
Failed to validate 429 41: (= (select a d) (select (store #33 #36 #37) (bvadd c d))) true
35: (select a d)
#x01
40: (select (store (store #30 #31 #32) (bvshl bv[1:32] #31) (select #33 #31)) (bvadd c d))
#x01
Failed to validate 434 45: (= (bvnot (if #41 bv[1:1] bv[0:1])) bv[0:1]) true
44: (bvnot (if (= #35 #40) bv[1:1] bv[0:1]))
#b0
5: bv[0:1]
#b0
sat
(error "line 10 column 10: an invalid model was generated")
[592] % cat small.smt2
(declare-fun a () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun b () (_ BitVec 32))
(declare-fun c () (_ BitVec 32))
(declare-fun d () (_ BitVec 32))
(assert
 (let ((e (store a c (select a b))) (f b) (k (bvadd (_ bv1 32))))
  (let ((g (store e k (e f))) (h (bvadd (_ bv1 32))) (i (bvadd k)))
   (let ((j (store g i (g h))))
    (not (= (bvnot (ite (= (select a d) (select (store j (bvshl (_ bv1 32) i) (j (bvadd  h))) (bvadd c d))) (_ bv1 1) (_ bv0 1))) (_ bv0 1)))))))
(check-sat)
[593] % 

[zhendongsu]

Invalid model:

[550] % z3release model_validate=true tactic.default_tactic=smt sat.euf=true small.smt2
sat
(error "line 9 column 10: an invalid model was generated")
[551] % cat small.smt2
(set-option :sat.local_search true)
(declare-sort a)
(declare-fun b (a a) Bool)
(declare-fun c () a)
(declare-fun d () a)
(declare-fun g () a)
(define-fun f () Bool (b g d))
(assert (xor f (b g c)))
(check-sat)
[552] % 

[zhendongsu]

Refutation unsoundness:

[534] % z3release small.smt2
sat
[535] % z3release tactic.default_tactic=smt sat.euf=true small.smt2
unsat
[536] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(assert (= (< (- a b) 0) (and false (>= a b))))
(check-sat)
[537] % 

[rainoftime]

src/sat/tactic/goal2sat.cpp:291

(set-option :rewriter.eq2ineq true)
(assert (forall ((X (_ FloatingPoint 2 2))) (= X ((_ to_fp 2 2) roundTowardZero (/ 0.0 1.0)))))
(check-sat)

z3 tactic.default_tactic=smt sat.euf=true delta.out.smt2
ASSERTION VIOLATION
File: ../src/sat/tactic/goal2sat.cpp
Line: 291
!m_app2lit.contains(t)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[rainoftime]

src/ast/rewriter/rewriter_def.h:50

(declare-fun C () (Array Bool Int))
(assert (forall ((A1 (Array (Array Int Bool) (Array Bool Int)))) (forall ((B (Array Int Bool))) (forall ((p Bool)) (= C (A1 (store B 1 p)))))))
(check-sat)

z3 tactic.default_tactic=smt sat.euf=true delta.out.smt2
ASSERTION VIOLATION
File: ../src/ast/rewriter/rewriter_def.h
Line: 50
v->get_sort() == r->get_sort()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[rainoftime]

src/math/simplex/model_based_opt.cpp:1129

(assert (forall ((x Int)) (= 0 (mod x 2))))
(check-sat)

z3 tactic.default_tactic=smt sat.euf=true delta.out.smt2
ASSERTION VIOLATION
File: ../src/math/simplex/model_based_opt.cpp
Line: 1129
!compute_def || eval(result) == eval(x)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[rainoftime]

model_based_opt.cpp：180

(assert (forall ((yuscore2dollarskuscore56 Real)) (or (> yuscore2dollarskuscore56 0.0) (= yuscore2dollarskuscore56 0.0))))
(check-sat-using ufbv)

z3 tactic.default_tactic=smt sat.euf=true delta.out.smt2
ASSERTION VIOLATION
File: ../src/math/simplex/model_based_opt.cpp
Line: 180
r.m_value == eval(r)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[NikolajBjorner]

These are now taken care of.
This helps a lot. There should be several more lurking around.