@@ -299,15 +299,11 @@ const IR::Literal *Z3Solver::toLiteral(const z3::expr &e, const IR::Type *type)
299299}
300300
301301void Z3Solver::toJSON (JSONGenerator &json) const {
302- json << json.indent << " {\n " ;
303- json.indent ++;
304- json << json.indent << " \" checkpoints\" : " << checkpoints;
305- json << " ,\n " ;
306- json << json.indent << " \" declarations\" : " << declaredVarsById;
307- json << " ,\n " ;
308- json << json.indent << " \" assertions\" : " << p4Assertions;
309- json.indent --;
310- json << json.indent << " }\n " ;
302+ auto state = json.begin_object ();
303+ json.emit (" checkpoints" , checkpoints);
304+ json.emit (" declarations" , declaredVarsById);
305+ json.emit (" assertions" , p4Assertions);
306+ json.end_object (state);
311307}
312308
313309void Z3Solver::addZ3Pushes (size_t &chkIndex, size_t asrtIndex) {
@@ -344,13 +340,13 @@ Z3Solver::Z3Solver(bool isIncremental, std::optional<std::istream *> inOpt)
344340 JSONLoader loader (*inOpt.value ());
345341
346342 JSONLoader solverCheckpoints (loader, " checkpoints" );
347- BUG_CHECK (solverCheckpoints.json -> is <JsonVector>(),
343+ BUG_CHECK (solverCheckpoints.is <JsonVector>(),
348344 " Z3 solver loading: can't find list of checkpoint" );
349345 solverCheckpoints >> checkpoints;
350346
351347 // loading all assertions
352348 JSONLoader solverAssertions (loader, " assertions" );
353- BUG_CHECK (solverAssertions.json -> is <JsonVector>(),
349+ BUG_CHECK (solverAssertions.is <JsonVector>(),
354350 " Z3 solver loading: can't find list of assertions" );
355351 safe_vector<const Constraint *> assertions;
356352 solverAssertions >> assertions;
0 commit comments