From 9968f5c97166ad40caa91283905837605b5100cb Mon Sep 17 00:00:00 2001 From: Houtan Bastani Date: Tue, 23 Oct 2018 14:00:36 +0200 Subject: [PATCH] fix bug in JSON output: JSON values that are decimals must be preceded by a 0 e.g. 0.5 is valid but .5 is not. --- src/ExprNode.cc | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/ExprNode.cc b/src/ExprNode.cc index 2df5e3bf..27fd7876 100644 --- a/src/ExprNode.cc +++ b/src/ExprNode.cc @@ -359,7 +359,11 @@ NumConstNode::writeOutput(ostream &output, ExprNodeOutputType output_type, void NumConstNode::writeJsonAST(ostream &output) const { - output << "{\"node_type\" : \"NumConstNode\", \"value\" : " << datatree.num_constants.get(id) << "}"; + output << "{\"node_type\" : \"NumConstNode\", \"value\" : "; + double testval = datatree.num_constants.getDouble(id); + if (testval < 1.0 && testval > -1.0 && testval != 0.0) + output << "0"; + output << datatree.num_constants.get(id) << "}"; } void