[Consolidated] Issutes related to tactic.default_tactic=smt sat.euf=true

[rainoftime]

SEGV ../src/sat/smt/bv_invariant.cpp:63 Hi, for the following formula, z3 4c4810c6113a

(set-option :model_validate true)
(declare-fun bv_28-0 () (_ BitVec 1))
(minimize bv_28-0)
(check-sat)

z3 tactic.default_tactic=smt sat.euf=true delta.out.smt2 
ASAN:SIGSEGV
=================================================================
==86585==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000000 (pc 0x00000162b3f0 bp 0x7ffcbd281ce0 sp 0x7ffcbd281b20 T0)
    #0 0x162b3ef in bv::solver::check_zero_one_bits(int) ../src/sat/smt/bv_invariant.cpp:63
    #1 0x15ff546 in bv::solver::after_merge_eh(int, int, int, int) (/home/peisen/test/tofuzz/z3-debug/build/z3+0x15ff546)
    #2 0x16003de in union_find<bv::solver, euf::solver>::merge(unsigned int, unsigned int) ../src/util/union_find.h:133
    #3 0x15f9568 in bv::solver::clone(euf::solver&) ../src/sat/smt/bv_solver.cpp:666
    #4 0x15a8664 in euf::solver::copy(sat::solver*) ../src/sat/smt/euf_solver.cpp:718
    #5 0x22f0eef in sat::solver::copy(sat::solver const&, bool) ../src/sat/sat_solver.cpp:177
    #6 0x22fe0f5 in sat::solver::check(unsigned int, sat::literal const*) ../src/sat/sat_solver.cpp:1307
    #7 0xae4355 in inc_sat_solver::check_sat_core(unsigned int, expr* const*) ../src/sat/sat_solver/inc_sat_solver.cpp:215
    #8 0x1bb8088 in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:332
    #9 0x5fa264 in solver::check_sat(ref_vector<expr, ast_manager> const&) ../src/solver/solver.h:161
    #10 0x5faf54 in opt::maxlex::maxlexN() ../src/opt/maxlex.cpp:159
    #11 0x5fb4ff in opt::maxlex::operator()() ../src/opt/maxlex.cpp:198
    #12 0x5d00cf in opt::maxsmt::operator()() ../src/opt/maxsmt.cpp:264
    #13 0x592acd in opt::context::execute_maxsat(symbol const&, bool, bool) ../src/opt/opt_context.cpp:436
    #14 0x592e27 in opt::context::execute(opt::context::objective const&, bool, bool) ../src/opt/opt_context.cpp:450
    #15 0x591470 in opt::context::optimize(ref_vector<expr, ast_manager> const&) ../src/opt/opt_context.cpp:336
    #16 0x1b700d2 in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1605
    #17 0x1b1b223 in smt2::parser::parse_check_sat() ../src/parsers/smt2/smt2parser.cpp:2605
    #18 0x1b1f17f in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2947
    #19 0x1b20877 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3139
    #20 0x1aff57e in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3188
    #21 0x43ede7 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:142
    #22 0x466d54 in main ../src/shell/main.cpp:372
    #23 0x7fd589a0583f in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x2083f)
    #24 0x416118 in _start (/home/peisen/test/tofuzz/z3-debug/build/z3+0x416118)

AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV ../src/sat/smt/bv_invariant.cpp:63 bv::solver::check_zero_one_bits(int)

[rainoftime]

Assertion error at ../src/ast/euf/euf_egraph.cpp:768

(set-logic QF_LIA)
(set-option :opt.priority pareto)
(set-option :model_validate true)
(declare-fun i1 () Int)
(declare-fun i3 () Int)
(declare-fun i5 () Int)
(declare-fun i14 () Int)
(maximize (- i1 i5 i14))
(maximize (- i1 i3 i5))
(check-sat)

z3 tactic.default_tactic=smt sat.euf=true delta.out.smt2 
ASSERTION VIOLATION
File: ../src/ast/euf/euf_egraph.cpp
Line: 768
src.m_scopes.empty()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)

Commit: 4c4810c

[rainoftime]

Assertion error at src/sat/smt/arith_solver.cpp:831

 (declare-fun v5 () Bool)
 (declare-fun i1 () Int)
 (declare-fun i2 () Int)
 (declare-fun i4 () Int)
 (declare-fun i5 () Int)
 (declare-fun i6 () Int)
 (declare-fun i9 () Int)
 (declare-fun i10 () Int)
 (assert (or (not (=> (= 23 i6 i4 i2 85) v5)) (<= i1 8 i9 i9 (+ (+ i1 349 i10 i6) i5)) (>= i4 782)))
 (check-sat)

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

Commit: 4c4810c

[rainoftime]

SEGV ../src/sat/smt/bv_solver.cpp:734

(set-option :model_validate true)
(declare-fun v7 () Bool)
(declare-fun bv_26-0 () (_ BitVec 3))
(assert (= (_ bv0 3) (bvudiv (_ bv0 3) bv_26-0)))
(assert-soft v7)
(check-sat)

ASAN:SIGSEGV
=================================================================
==77086==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000000 (pc 0x0000015fa6ff bp 0x7ffc270827c0 sp 0x7ffc27082690 T0)
    #0 0x15fa6fe in bv::solver::merge_eh(int, int, int, int) ../src/sat/smt/bv_solver.cpp:734
    #1 0x16001d9 in union_find<bv::solver, euf::solver>::merge(unsigned int, unsigned int) ../src/util/union_find.h:128
    #2 0x15f9568 in bv::solver::clone(euf::solver&) ../src/sat/smt/bv_solver.cpp:666
    #3 0x15a8664 in euf::solver::copy(sat::solver*) ../src/sat/smt/euf_solver.cpp:718
    #4 0x22f0eef in sat::solver::copy(sat::solver const&, bool) ../src/sat/sat_solver.cpp:177
    #5 0x22fe0f5 in sat::solver::check(unsigned int, sat::literal const*) ../src/sat/sat_solver.cpp:1307
    #6 0xae4355 in inc_sat_solver::check_sat_core(unsigned int, expr* const*) ../src/sat/sat_solver/inc_sat_solver.cpp:215
    #7 0x1bb8088 in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:332
    #8 0x5fa264 in solver::check_sat(ref_vector<expr, ast_manager> const&) ../src/solver/solver.h:161
    #9 0x5faf54 in opt::maxlex::maxlexN() ../src/opt/maxlex.cpp:159
    #10 0x5fb4ff in opt::maxlex::operator()() ../src/opt/maxlex.cpp:198
    #11 0x5d00cf in opt::maxsmt::operator()() ../src/opt/maxsmt.cpp:264
    #12 0x592acd in opt::context::execute_maxsat(symbol const&, bool, bool) ../src/opt/opt_context.cpp:436
    #13 0x592e27 in opt::context::execute(opt::context::objective const&, bool, bool) ../src/opt/opt_context.cpp:450
    #14 0x591470 in opt::context::optimize(ref_vector<expr, ast_manager> const&) ../src/opt/opt_context.cpp:336
    #15 0x1b700d2 in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1605
    #16 0x1b1b223 in smt2::parser::parse_check_sat() ../src/parsers/smt2/smt2parser.cpp:2605
    #17 0x1b1f17f in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2947
    #18 0x1b20877 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3139
    #19 0x1aff57e in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3188
    #20 0x43ede7 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:142
    #21 0x466d54 in main ../src/shell/main.cpp:372
    #22 0x7f8f20cf383f in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x2083f)
    #23 0x416118 in _start (/home/peisen/test/tofuzz/z3-debug/build/z3+0x416118)

AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV ../src/sat/smt/bv_solver.cpp:734 bv::solver::merge_eh(int, int, int, int)
==77086==ABORTING

Commit: 4c4810c

[rainoftime]

Assertion error at src/sat/smt/bv_internalize.cpp:234

(set-logic QF_UFBV)
(assert (distinct ((_ repeat 5) (_ bv0 44)) (_ bv0 220) (_ bv0 220)))
(check-sat)

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

[rainoftime]

Invalid models

(declare-const x1 Real)
(declare-const x2 Real)
(declare-const x3 Real)
(declare-const x4 Real)
(declare-const x5 Real)
(assert (and (>= x1 0.0) (<= x2 0.0) (> x3 0.0) (= (* x1 x2) 1.0) (= (+ (* x1 x3) x2 (- (- 1.0) x3)) 2.0)))
(check-sat)
(reset)
(set-logic QF_NRA)
(declare-const x1 Real)
(declare-const x2 Real)
(declare-const x3 Real)
(declare-const x4 Real)
(declare-const x5 Real)
(assert (and (<= x1 0.0) (> x2 0.0) (>= x3 0.0) (distinct (+ x1 x2) 1.0) (distinct (* (+ x1 x3) x2 (* (- 1.0) x3)) 2.0)))
(check-sat)

unsat
Failed to validate 41: (= (+ x1 x2) 1.0) true
sat
(error "line 16 column 10: an invalid model was generated")

---

(declare-fun |ku'0'| () Int)
(declare-fun |ku'1'| () Int)
(declare-fun |ku'4'| () Int)
(declare-fun |ku'3'| () Int)
(declare-fun |ku'2'| () Int)
(assert (and (> |ku'0'| 0) (> |ku'0'| 1)))
(assert (distinct |ku'0'| 1))
(assert (or (>= |ku'1'| 0) (<= |ku'1'| 1)))
(assert (>= (* |ku'1'| |ku'2'| |ku'3'| |ku'4'|) 1))
(assert (or (>= |ku'2'| 0) (> |ku'2'| 1)))
(assert (> (+ |ku'2'| |ku'3'|) 1))
(assert (or (<= |ku'3'| 0) (> |ku'3'| 1)))
(assert (>= (- |ku'3'| |ku'2'|) 1))
(assert (or (<= |ku'4'| 0) (<= |ku'4'| 1)))
(assert (> (+ |ku'4'| |ku'2'| |ku'3'|) 1))
(minimize (+ |ku'0'| |ku'1'| |ku'2'| |ku'3'| |ku'4'|))
(check-sat)

[rainoftime]

Memory leak

(declare-datatypes () ((Tuple (tuple (_f (_ FloatingPoint 2 2))))))
(declare-const X Tuple)
(assert (= (_f X) (_ +zero 2 2)))
(check-sat)

z3 tactic.default_tactic=smt sat.euf=true delta.out.smt2 
sat

=================================================================
==176864==ERROR: LeakSanitizer: detected memory leaks

Indirect leak of 80 byte(s) in 2 object(s) allocated from:
    #0 0x7f271ed1f662 in malloc (/usr/lib/x86_64-linux-gnu/libasan.so.2+0x98662)
    #1 0x2849ceb in memory::allocate(unsigned long) ../src/util/memory_manager.cpp:273
    #2 0x284980e in memory::allocate(char const*, int, char const*, unsigned long) ../src/util/memory_manager.cpp:212
    #3 0x1663b8f in bv::ackerman::new_tmp() ../src/sat/smt/bv_ackerman.cpp:127
    #4 0x1662b69 in bv::ackerman::used_eq_eh(int, int) ../src/sat/smt/bv_ackerman.cpp:51
    #5 0x15f1500 in bv::solver::add_fixed_eq(int, int) ../src/sat/smt/bv_solver.cpp:91
    #6 0x15f126f in bv::solver::fixed_var_eh(int) ../src/sat/smt/bv_solver.cpp:83
    #7 0x15f1b18 in bv::solver::find_wpos(int) ../src/sat/smt/bv_solver.cpp:128
    #8 0x15f6b4e in bv::solver::propagate_bits(std::pair<int, unsigned int>) ../src/sat/smt/bv_solver.cpp:448
    #9 0x15f5bea in bv::solver::unit_propagate() ../src/sat/smt/bv_solver.cpp:404
    #10 0x15a397b in euf::solver::unit_propagate() ../src/sat/smt/euf_solver.cpp:336
    #11 0x22fa681 in sat::solver::propagate_core(bool) ../src/sat/sat_solver.cpp:1033
    #12 0x22fa8c2 in sat::solver::propagate(bool) ../src/sat/sat_solver.cpp:1045
    #13 0x2303842 in sat::solver::basic_search() ../src/sat/sat_solver.cpp:1718
    #14 0x2303a6a in sat::solver::search() ../src/sat/sat_solver.cpp:1731
    #15 0x23036aa in sat::solver::bounded_search() ../src/sat/sat_solver.cpp:1711
    #16 0x22fe781 in sat::solver::check(unsigned int, sat::literal const*) ../src/sat/sat_solver.cpp:1341
    #17 0x151717e in sat_tactic::imp::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/sat/tactic/sat_tactic.cpp:66
    #18 0x1518a84 in sat_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/sat/tactic/sat_tactic.cpp:202
    #19 0x1c36be5 in cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:924
    #20 0x1c29e68 in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:150
    #21 0x1c2a303 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_ma
nager>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >&) ../src/tactic/tactic.cpp:170
    #22 0x1ba9f3a in check_sat_core2 ../src/solver/tactic2solver.cpp:187
    #23 0x1bb3deb in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
    #24 0x1bbafc6 in combined_solver::check_sat_core(unsigned int, expr* const*) ../src/solver/combined_solver.cpp:252
    #25 0x1bb8088 in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:332

[rainoftime]

Assertion error at src/math/lp/lar_solver.cpp:1183

(set-logic QF_LIA)
(set-option :model_validate true)
(set-option :sat.threads 4)
(declare-fun i4 () Int)
(declare-fun v42 () Bool)
(assert (and (> 4 i4) true))
(check-sat-using (then add-bounds qfaufbv))

ASSERTION VIOLATION
File: ../src/math/lp/lar_solver.cpp
Line: 1183
get_status() == lp_status::OPTIMAL || get_status() == lp_status::FEASIBLE
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[rainoftime]

Non-deterministic heap-use-after-free

(set-option :model_validate true)
(set-option :sat.threads 4)
(declare-fun bv_34-0 () (_ BitVec 34))
(assert-soft (bvule bv_34-0 (_ bv1 34)) :weight 7)
v8
1
(check-sat)

(error "line 5 column 0: invalid command, '(' expected")
sat
=================================================================
==180458==ERROR: AddressSanitizer: heap-use-after-free on address 0x607000008290 at pc 0x000000446d4a bp 0x7ffe2e631e40 sp 0x7ffe2e631e30
READ of size 4 at 0x607000008290 thread T0
    #0 0x446d49 in ast::dec_ref() ../src/ast/ast.h:495
    #1 0x446ecc in ast_manager::dec_ref(ast*) ../src/ast/ast.h:1637
    #2 0x45050c in ref_manager_wrapper<expr, ast_manager>::dec_ref(expr*) ../src/util/ref_vector.h:221
    #3 0x44f8b8 in ref_vector_core<expr, ref_manager_wrapper<expr, ast_manager> >::dec_ref(expr*) ../src/util/ref_vector.h:36
    #4 0x44d8f6 in ref_vector_core<expr, ref_manager_wrapper<expr, ast_manager> >::dec_range_ref(expr* const*, expr* const*) ../src/util/ref_vector.h:40
    #5 0x44b565 in ref_vector_core<expr, ref_manager_wrapper<expr, ast_manager> >::~ref_vector_core() ../src/util/ref_vector.h:61
    #6 0x447fb3 in ref_vector<expr, ast_manager>::~ref_vector() ../src/util/ref_vector.h:232
    #7 0x151bf28 in sat2goal::mc::~mc() ../src/sat/tactic/goal2sat.h:97
    #8 0x453ade in void deallocf<converter>(char const*, int, converter*) ../src/util/memory_manager.h:85
    #9 0x45311c in converter::dec_ref() ../src/tactic/converter.h:36
    #10 0x4552a7 in ref<sat2goal::mc>::dec_ref() ../src/util/ref.h:34
    #11 0x453f81 in ref<sat2goal::mc>::~ref() ../src/util/ref.h:58
    #12 0xae24a6 in inc_sat_solver::~inc_sat_solver() (/home/peisen/test/tofuzz/z3-debug/build/z3+0xae24a6)
    #13 0x4831cb in void deallocf<check_sat_result>(char const*, int, check_sat_result*) ../src/util/memory_manager.h:85
    #14 0x47a784 in check_sat_result::dec_ref() ../src/solver/check_sat_result.h:50
    #15 0x4844df in ref<solver>::dec_ref() ../src/util/ref.h:34
    #16 0x483269 in ref<solver>::~ref() ../src/util/ref.h:58
    #17 0x58fc46 in opt::context::~context() ../src/opt/opt_context.cpp:152
    #18 0x4831cb in void deallocf<check_sat_result>(char const*, int, check_sat_result*) ../src/util/memory_manager.h:85
    #19 0x47a784 in check_sat_result::dec_ref() ../src/solver/check_sat_result.h:50
    #20 0x1b81787 in ref<opt_wrapper>::dec_ref() ../src/util/ref.h:34
    #21 0x1b7cbc4 in ref<opt_wrapper>::operator=(opt_wrapper*) ../src/util/ref.h:84
    #22 0x1b6d5a2 in cmd_context::reset(bool) ../src/cmd_context/cmd_context.cpp:1361
    #23 0x1b64638 in cmd_context::~cmd_context() ../src/cmd_context/cmd_context.cpp:563
    #24 0x43ee97 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:122
    #25 0x466d54 in main ../src/shell/main.cpp:372
    #26 0x7f04b3dd383f in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x2083f)
    #27 0x416118 in _start (/home/peisen/test/tofuzz/z3-debug/build/z3+0x416118)

[rainoftime]

Assertion error at src/ast/euf/euf_egraph.cpp:287

 (declare-fun i0 () Int)
 (declare-fun i2 () Int)
 (declare-fun i3 () Int)
 (declare-fun i4 () Int)
 (declare-fun i5 () Int)
 (declare-fun i8 () Int)
 (assert (>= i3 (abs 26)))
 (minimize (+ i0 i2 i4))
 (maximize (- i2 i5 i8))
 (check-sat)

ASSERTION VIOLATION
File: ../src/ast/euf/euf_egraph.cpp
Line: 287
n->value() == l_undef
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[rainoftime]

Assertion error at src/sat/smt/euf_internalize.cpp:145

(set-logic QF_UFBV)
(assert (distinct (not false) true true))
(check-sat)

z3 tactic.default_tactic=smt sat.euf=true xx.smt2
ASSERTION VIOLATION
File: ../src/sat/smt/euf_internalize.cpp
Line: 145
m_egraph.find(e)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[rainoftime]

Nondeterministic assertion error at ./src/util/vector.h:474

(set-logic QF_UFBV)
(declare-fun _substvar_6_ () Bool)
(set-option :sat.threads 3)
(set-option :parallel.simplify.exp 4)
(set-option :smt.random_seed 2)
(declare-fun v14 () Bool)
(declare-fun v17 () Bool)
(declare-fun v51 () Bool)
(declare-fun v85 () Bool)
(assert true)
(assert _substvar_6_)
(check-sat-using (then sat-preprocess eq2bv fix-dl-var reduce-bv-size macro-finder ackermannize_bv solve-eqs normalize-bounds uflra))

ASSERTION VIOLATION
File: ../src/util/vector.h
Line: 474
idx < size()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[rainoftime]

Assertion error at /src/sat/smt/euf_model.cpp:204

(set-logic QF_UFBV)
(set-option :sat.threads 3)
(set-option :fp.datalog.compile_with_widening true)
(declare-fun uf4_2 (Bool Bool Bool Bool) Bool)
(declare-fun v1 () Bool)
(declare-fun v4 () Bool)
(declare-fun v8 () Bool)
(declare-fun v10 () Bool)
(assert (uf4_2 true (and true true true v10) true true))
(check-sat)

peisen@chcpu11:~/work/smt-fuzz$ ~/test/tofuzz/z3-debug/build/z3 tactic.default_tactic=smt sat.euf=true xx.smt2
ASSERTION VIOLATION
File: ../src/sat/smt/euf_model.cpp
Line: 204
Failed to verify: arg

[rainoftime]

Assertion error at /src/ast/euf/euf_egraph.cpp:501

(set-logic QF_UFBV)
(set-option :sat.branching.anti_exploration true)
(set-option :sat.force_cleanup true)
(declare-fun bv_8-0 () (_ BitVec 8))
(declare-fun bv_41-0 () (_ BitVec 41))
(maximize (bvlshr bv_8-0 bv_8-0))
(minimize (bvmul bv_41-0 (bvneg bv_41-0)))
(minimize (bvsrem (bvneg bv_41-0) (bvmul bv_41-0 (bvneg bv_41-0))))
(check-sat)

ASSERTION VIOLATION
File: ../src/ast/euf/euf_egraph.cpp
Line: 501
m_num_scopes == 0 || m_to_merge.empty()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[rainoftime]

Assertion error at src/ast/euf/euf_enode.h:166

(set-logic QF_UFBV)
(declare-fun uf7 (Bool Bool Bool Bool Bool Bool Bool) Bool)
(declare-fun v7 () Bool)
(declare-fun v9 () Bool)
(assert (= true true true true (uf7 true true v9 true v9 (xor v9 true true v7) true)))
(maximize (_ bv0 16))
(check-sat)

ASSERTION VIOLATION
File: ../src/ast/euf/euf_enode.h
Line: 166
i < num_args()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[NikolajBjorner]

it is somewhat premature to try multi-threaded options. A large amount of bugs should manifest already without threads.

[NikolajBjorner]

These ones are handled. Better to open a new thread for next ones.