1--TEST--
2Bug #41567 (json_encode() double conversion is inconsistent with PHP)
3--INI--
4serialize_precision=-1
5--FILE--
6<?php
7
8$a = json_encode(123456789.12345);
9var_dump(json_decode($a));
10
11echo "Done\n";
12?>
13--EXPECT--
14float(123456789.12345)
15Done
16
