mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-10 05:00:51 +00:00
Code Activity

disambiguate call

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-30 13:35:40 -07:00
parent 5152c9500d
commit 53b5ca3c2b
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/theory_arith_nl.h
View file

@ -811,7 +811,7 @@ bool theory_arith<Ext>::branch_nl_int_var(theory_var v) {
} }
ctx.internalize(bound, true); ctx.internalize(bound, true);
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
ctx.mark_as_relevant(bound); ctx.mark_as_relevant(bound.get());
literal l = ctx.get_literal(bound); literal l = ctx.get_literal(bound);
SASSERT(!l.sign()); SASSERT(!l.sign());
ctx.set_true_first_flag(l.var()); // force the context to case split to true first, independently of the phase selection strategy. ctx.set_true_first_flag(l.var()); // force the context to case split to true first, independently of the phase selection strategy.