mirror of
https://github.com/Z3Prover/z3
synced 2025-04-29 11:55:51 +00:00
Managed API: Refactoring
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
parent
d1342ba7a9
commit
8c32f6b015
3 changed files with 6 additions and 6 deletions
|
@ -184,10 +184,10 @@ namespace Microsoft.Z3
|
|||
{
|
||||
Tactic t = Context.MkTactic("simplify");
|
||||
ApplyResult res = t.Apply(this, p);
|
||||
|
||||
|
||||
if (res.NumSubgoals == 0)
|
||||
return Context.MkGoal();
|
||||
else
|
||||
throw new Z3Exception("No subgoals");
|
||||
else
|
||||
return res.Subgoals[0];
|
||||
}
|
||||
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue