mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 05:48:44 +00:00
Code Activity

regression fix

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2018-06-29 16:10:15 -07:00
parent 4d88818560
commit 16d4e2f5d1
1 changed files with 0 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/smt/theory_lra.cpp
View file

@ -862,9 +862,6 @@ public:
if (ctx().e_internalized(term) && th.is_attached_to_var(ctx().get_enode(term))) { if (ctx().e_internalized(term) && th.is_attached_to_var(ctx().get_enode(term))) {
// skip // skip
} }
else if (a.is_numeral(term)) {
mk_enode(term);
}
else { else {
internalize_def(term); internalize_def(term);
} }