Fix the order of formulas printed by the z3 mapping printer

[hra687261]

Simply selects the last assert in the list, and adds all the other ones as assumptions (which why we redo a List.rev on the tail of the reversed list).

If we test by running smtml to-smt2 on

smtml/test/cli/smtml/test_lia.smtml

Lines 1 to 16 in 7e1e145

	;(set-logic LIA)
	(let-const x int)
	(let-const y int)
	(let-const z int)
	(assert (int.gt x 0))
	(assert (int.le x 10))
	(assert (= (int.sub (int.add x y) y) x))
	(assert (= (int.div (int.mul x y) y) x))
	(assert (int.lt (int.rem y x) 10))
	(assert
	(=
	(int.div (int.pow x 2) x)
	(int.div (int.mul x x) x)))
	(check-sat)
	(assert (int.lt (int.neg z) 0))
	(check-sat)

With this fix the result is:

New result

; test_lia.smtml
(set-info :status unknown)
(set-logic ALL)
(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun z () Int)
(assert
 (< 0 x))
(assert
 (<= x 10))
(assert
 (let ((?x16 (+ x y)))
 (let ((?x17 (- ?x16 y)))
 (= ?x17 x))))
(assert
 (let ((?x19 (* x y)))
 (let ((?x20 (div ?x19 y)))
 (= ?x20 x))))
(assert
 (let ((?x22 (rem y x)))
 (< ?x22 10)))
(assert
 (let ((?x25 (^ x 2)))
 (let ((?x27 (/ ?x25 (to_real x))))
 (= ?x27 (to_real (div (* x x) x))))))
(assert
 (let ((?x33 (- z)))
(< ?x33 0)))
(check-sat)

While in the original it was:

Old result

; test_lia.smtml
(set-info :status unknown)
(set-logic ALL)
(declare-fun z () Int)
(declare-fun x () Int)
(declare-fun y () Int)
(assert
 (let ((?x33 (- z)))
 (< ?x33 0)))
(assert
 (let ((?x25 (^ x 2)))
 (let ((?x27 (/ ?x25 (to_real x))))
 (= ?x27 (to_real (div (* x x) x))))))
(assert
 (let ((?x22 (rem y x)))
 (< ?x22 10)))
(assert
 (let ((?x19 (* x y)))
 (let ((?x20 (div ?x19 y)))
 (= ?x20 x))))
(assert
 (let ((?x16 (+ x y)))
 (let ((?x17 (- ?x16 y)))
 (= ?x17 x))))
(assert
 (<= x 10))
(assert
 (< 0 x))
(check-sat)

Notice that one of the check-sats is lost, that is because it is filtered out in:

smtml/src/bin/cmd_to_smt2.ml

Lines 9 to 11 in 7e1e145

	let assertions =
	List.filter_map (function Ast.Assert e -> Some e | _ -> None) ast
	in

[filipeom]

Thanks! I never actually tested the printer was correct 😅

Notice that one of the check-sats is lost, that is because it is filtered out in:

Yes, this is unfortunate I'll create an issue for in in the time being