mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
fix else case: it is first argument of const array
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
35d26bc282
commit
676ba78600
|
@ -276,7 +276,7 @@ namespace Microsoft.Z3
|
|||
if (kind == Z3_decl_kind.Z3_OP_CONST_ARRAY)
|
||||
{
|
||||
result = new ArrayValue();
|
||||
result.Else = r;
|
||||
result.Else = ntvContext.GetAppArg(r, 0);
|
||||
result.Updates = updates.ToArray();
|
||||
result.Domain = updates.Keys.ToArray();
|
||||
result.Range = updates.Values.ToArray();
|
||||
|
|
Loading…
Reference in a new issue