Segfault in fixpoint engine when built with g++-4.9.2

[dfoxfranke]

On at least the master, unstable, and opt branches, z3 segfaults on the following input when it is built with g++-4.9.2 on Debian Jessie for x86-64:

(declare-rel reach (Int Int))
(declare-var x Int)
(declare-var y Int)


(rule (reach x x))
(rule (=> (and (reach (div x 2) y) (= (mod x 2) 0)) (reach x y)))
(rule (=> (and (reach (+ (* x 3) 1) y) (= (mod x 2) 1)) (reach x y)))

(query (reach 3 1) :print-answer true)

Backtrace:

#0  0x00000000010947a3 in memory::deallocate(void*) ()
#1  0x00000000006d1777 in datalog::mk_slice::get_predicate_slice(func_decl*) ()
#2  0x00000000006d1f18 in datalog::mk_slice::init_vars(app*, bool, bool) ()
#3  0x00000000006d209b in datalog::mk_slice::init_vars(datalog::rule&) ()
#4  0x00000000006d2259 in datalog::mk_slice::prune_rule(datalog::rule&) ()
#5  0x00000000006d3cab in datalog::mk_slice::operator()(datalog::rule_set const&) ()
#6  0x000000000072e99b in datalog::rule_transformer::operator()(datalog::rule_set&)
    ()
#7  0x0000000000735236 in datalog::context::transform_rules(datalog::rule_transformer&) ()
#8  0x000000000058931c in pdr::dl_interface::query(expr*) ()
#9  0x00000000005386c4 in dl_query_cmd::execute(cmd_context&) ()
#10 0x0000000000b94276 in smt2::parser::parse_ext_cmd() ()
#11 0x0000000000b9548c in smt2::parser::operator()() ()
#12 0x0000000000b86178 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&) ()
#13 0x0000000000422ee6 in read_smtlib2_commands(char const*) ()
#14 0x000000000040ded3 in main ()

However, if I compile z3 on Debian Wheezy with g++-4.7.2 and then copy the binary onto my Debian Jessie system and run it there with the same input, it works fine!

[dfoxfranke]

It also works fine if I compile with g++-4.6.4 on the Jessie system, so this definitely has to do with the compiler version and not any other difference between the two systems.

[wintersteiger]

For reference: possible duplicate of this.

[NikolajBjorner]

It's a compiler bug, see duplicate.

[nunoplopes]

My analysis was wrong. Z3 is executing undefined behavior and gcc is taking advantage of that.