mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 11:42:28 +00:00
Code Activity

update Deprecated API to avoid memory leak and crash when there is a core, ensure invariant in new code

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-10-07 19:54:04 -07:00
parent 06c7f3f246
commit a3a008bdde
2 changed files with 16 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/api/dotnet/Deprecated.cs
View file

@ -65,22 +65,29 @@ namespace Microsoft.Z3
/// <summary>
/// Checks whether the assertions in the context are consistent or not.
/// </summary>
public static Status Check(Context ctx, List<BoolExpr> core, params Expr[] assumptions)
public static Status Check(Context ctx, List<BoolExpr> core, ref Model model, ref Expr proof, params Expr[] assumptions)
{
Z3_lbool r;
core = null;
model = null;
proof = null;
if (assumptions == null || assumptions.Length == 0)
r = (Z3_lbool)Native.Z3_check(ctx.nCtx);
else {
IntPtr model = IntPtr.Zero, proof = IntPtr.Zero;
IntPtr mdl = IntPtr.Zero, prf = IntPtr.Zero;
uint core_size = 0;
IntPtr[] native_core = new IntPtr[assumptions.Length];
r = (Z3_lbool)Native.Z3_check_assumptions(ctx.nCtx,
(uint)assumptions.Length, AST.ArrayToNative(assumptions),
ref model, ref proof, ref core_size, native_core);
ref mdl, ref prf, ref core_size, native_core);
for (uint i = 0; i < core_size; i++)
core.Add((BoolExpr)Expr.Create(ctx, native_core[i]));
if (mdl != IntPtr.Zero) {
model = new Model(ctx, mdl);
}
if (prf != IntPtr.Zero) {
proof = Expr.Create(ctx, prf);
}
}
switch (r)

7
src/muz/rel/udoc_relation.cpp
View file

@ -1148,18 +1148,21 @@ namespace datalog {
utbv& neg = d->neg();
unsigned mid = dm1.num_tbits();
unsigned hi = dm.num_tbits();
tbm.set(pos,d1.pos(), mid-1, 0);
tbm.set(pos,d2.pos(), hi-1, mid);
tbm.set(pos, d1.pos(), mid-1, 0);
tbm.set(pos, d2.pos(), hi-1, mid);
for (unsigned i = 0; i < d1.neg().size(); ++i) {
t = tbm.allocateX();
tbm.set(*t, d1.neg()[i], mid-1, 0);
VERIFY(tbm.set_and(*t, pos));
neg.push_back(t.detach());
}
for (unsigned i = 0; i < d2.neg().size(); ++i) {
t = tbm.allocateX();
tbm.set(*t, d2.neg()[i], hi-1, mid);
VERIFY(tbm.set_and(*t, pos));
neg.push_back(t.detach());
}
SASSERT(dm.well_formed(*d));
return d.detach();
}