Skip to content

Commit 59013a7

Browse files
committed
Fix logging of queries after model generation
1 parent 11b51b5 commit 59013a7

File tree

1 file changed

+3
-2
lines changed

1 file changed

+3
-2
lines changed

src/smtml/mappings.ml

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -954,13 +954,14 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
954954
M.Solver.check s.solver ~ctx ~assumptions:encoded_assuptions )
955955
M.Internals.name (List.rev assumptions)
956956

957-
let model { solver; last_ctx; assumptions; _ } =
957+
let model { solver; last_ctx; assumptions; last_assumptions; _ } =
958958
match last_ctx with
959959
| Some ctx ->
960960
Utils.run_and_log_query ~model:true
961961
(fun () ->
962962
M.Solver.model solver |> Option.map (fun m -> { model = m; ctx }) )
963-
M.Internals.name (List.rev assumptions)
963+
M.Internals.name
964+
(List.rev_append assumptions (List.rev last_assumptions))
964965
| None ->
965966
Fmt.failwith "model: Trying to fetch model before check-sat call"
966967

0 commit comments

Comments
 (0)