Placeholder for get_assignments

src/bin/common/solving_loop.ml

@@ -537,11 +537,13 @@ let main () =
             st
       )
     | ":produce-assignments",  Symbol { name = Simple b; _ } ->
-      begin
-        match bool_of_string_opt b with
-        | None -> print_wrn_opt ~name:":verbosity" st_loc "integer" value
-        | Some b -> Options.set_produce_assignments b
-      end
+       let () =
+         match bool_of_string_opt b with
+         | None ->
+            print_wrn_opt ~name:":verbosity" st_loc "integer" value
+         | Some b ->
+            Options.set_produce_assignments b
+       in st
     | (":global-declarations"
       | ":interactive-mode"
       | ":produce-assertions"
@@ -655,6 +657,10 @@ let main () =
       unsupported_opt name
   in
 
+  let handle_get_assignment _ =
+    failwith "TODO: handle_get_assignment"
+  in
+
   let handle_stmt :
     Frontend.used_context -> State.t ->
     _ D_loop.Typer_Pipe.stmt -> State.t =
@@ -783,6 +789,16 @@ let main () =
         handle_get_info st kind;
         st
 
+      | {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
+
       | {contents = `Other (custom, args); _} ->
         handle_custom_statement custom args st