mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity

install importlib-resources for ubuntu doc

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-12-04 10:33:29 -08:00
parent de75692cb0
commit f98b42ae42
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/sat/smt/array_axioms.cpp
View file

@ -443,7 +443,8 @@ namespace array {
sel2 = a.mk_select(args2); sel2 = a.mk_select(args2);
return return
ctx.propagate(e_internalize(sel1), ndef1, array_axiom()) || ctx.propagate(e_internalize(sel1), ndef1, array_axiom()) ||
ctx.propagate(e_internalize(sel2), ndef2, array_axiom()); ctx.propagate(e_internalize(sel2), ndef2, array_axiom()) ||
prop;
} }
// default(A) == default(B) // default(A) == default(B)
if (ctx.propagate(ndef1, ndef2, array_axiom())) if (ctx.propagate(ndef1, ndef2, array_axiom()))