demonstrating difference in printing in z3

z3print.py

#!/usr/bin/env python3
import sys
import z3
s = z3.Solver()
s.from_file(sys.argv[1])
l = s.assertions()
for c in l:
    print(c.sexpr()) # this print command uses ast_smt2_pp
s.check()
print(s.to_smt2()) # this print command uses ast_smt_pp

If you run this code with z3master on this input, it will output:

(and ((_ is (mcons (Int MList) MList)) x) (= (mtail x) y) (= y mnill))
; benchmark generated from python API
(set-info :status unknown)
(declare-datatypes ((MList 0)) (((mcons (mhead Int) (mtail MList)) (mnill))))
 (declare-fun y () MList)
(declare-fun x () MList)
(assert
 (let (($x29 (= y mnill)))
 (let (($x27 (= (mtail x) y)))
 (let (($x24 ((_ is mcons ) x)))
 (and $x24 $x27 $x29)))))
 (check-sat)

The first line is the result of print on line 8 and the rest is the result of print on line 10. The first print uses src/ast/ast_smt2_pp.cpp to print. The second print uses src/ast/ast_smt_pp.cpp to print. The first print is invalid according to SMTlib. Z3 itself cannot parse it. The second print is valid and accepted by both z3 and cvc4