mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-23 12:48:53 +00:00
Code Activity

fix #3708

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-03 12:23:54 -07:00
parent cd2f6705aa
commit f92c6ad170
1 changed files with 3 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/smt/theory_utvpi_def.h
View file

@ -571,6 +571,9 @@ namespace smt {
context& ctx = get_context(); context& ctx = get_context();
if (r.is_zero()) { if (r.is_zero()) {
v = get_zero(n); v = get_zero(n);
if (!ctx.e_internalized(n)) {
v = null_theory_var;
}
} }
else if (ctx.e_internalized(n)) { else if (ctx.e_internalized(n)) {
enode* e = ctx.get_enode(n); enode* e = ctx.get_enode(n);