diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index 662305b10b..d816486a30 100644 --- a/src/bin/common/solving_loop.ml +++ b/src/bin/common/solving_loop.ml @@ -408,6 +408,10 @@ let main () = | _ -> Printer.print_wrn "unsupported option %s" name in + let handle_get_assignment _ = + failwith "TODO: handle_get_assignment" + in + let handle_stmt : FE.used_context -> State.t -> _ D_loop.Typer_Pipe.stmt -> State.t = @@ -509,6 +513,16 @@ let main () = st end + | {contents = `Get_assignment; _} -> + if Options.get_produce_assignments () then + handle_get_assignment () + else + begin + Printer.print_smtlib_err + "Produce assignments disabled; add (set-option :produce-assignment)"; + st + end + | _ -> (* TODO: - Separate statements that should be ignored from unsupported