mirror of
https://github.com/Z3Prover/z3
synced 2025-04-15 13:28:47 +00:00
misc
This commit is contained in:
parent
da9ed82889
commit
4549ec7331
|
@ -153,10 +153,8 @@ namespace Microsoft.Z3
|
||||||
prop.callback = cb;
|
prop.callback = cb;
|
||||||
prop.decide_eh(ref t, ref idx, ref phase);
|
prop.decide_eh(ref t, ref idx, ref phase);
|
||||||
prop.callback = IntPtr.Zero;
|
prop.callback = IntPtr.Zero;
|
||||||
if (u != t) {
|
if (u != t)
|
||||||
a = t.NativeObject;
|
a = t.NativeObject;
|
||||||
}
|
|
||||||
t.Dispose();
|
|
||||||
}
|
}
|
||||||
|
|
||||||
/// <summary>
|
/// <summary>
|
||||||
|
@ -203,9 +201,9 @@ namespace Microsoft.Z3
|
||||||
public virtual void Pop(uint n) { throw new Z3Exception("Pop method should be overwritten"); }
|
public virtual void Pop(uint n) { throw new Z3Exception("Pop method should be overwritten"); }
|
||||||
|
|
||||||
/// <summary>
|
/// <summary>
|
||||||
/// Virtual method for fresh. It must be overwritten by inherited class.
|
/// Virtual method for fresh. It can be overwritten by inherited class.
|
||||||
/// </summary>
|
/// </summary>
|
||||||
public virtual UserPropagator Fresh(Context ctx) { throw new Z3Exception("Fresh method should be overwritten"); }
|
public virtual UserPropagator Fresh(Context ctx) { return new UserPropagator(ctx); }
|
||||||
|
|
||||||
/// <summary>
|
/// <summary>
|
||||||
/// Declare combination of assigned expressions a conflict
|
/// Declare combination of assigned expressions a conflict
|
||||||
|
|
Loading…
Reference in a new issue