Named annotations appear in model generated by get-model

[edwardcwang]

Z3 emits named annotations/named assertions in the model generated by get-model with unsimplified values.
Other solvers only emit variables, not named annotations.

This creates issues / a need for postprocessing to remove the unwanted extra items in the model.

Consider the following example, where Z3 generated these extraneous lines in the model compared with other solvers.

  (define-fun named_assertion_2 () Bool
    true)
  (define-fun named_assertion_3 () Bool
    (not (<= xvar4 0)))
  (define-fun named_assertion_1 () Bool
    (or (<= xvar2 (+ 75 xvar3))
    (>= xvar2 (+ 250 xvar3))
    (<= xvar1 (+ 50 xvar3))
    (>= xvar1 (+ 250 xvar4))))

(set-option :produce-unsat-cores true)
(set-option :produce-models true)
(set-logic QF_LIA)
(declare-const xvar1 Int)
(declare-const xvar2 Int)
(declare-const xvar3 Int)
(declare-const xvar4 Int)
(assert (! (or (>= (+ 0 xvar1) (+ (+ 150 xvar4) 100)) (<= (+ (+ 0 xvar1) 100) (+ 150 xvar3)) (>= (+ 25 xvar2) (+ (+ 175 xvar3) 100)) (<= (+ (+ 25 xvar2) 75) (+ 175 xvar3))) :named named_assertion_1))
(assert (! (or (>= (+ 0 xvar4) (+ (+ 150 xvar4) 100)) (<= (+ (+ 0 xvar3) 100) (+ 150 xvar2)) (>= (+ 25 xvar3) (+ (+ 175 xvar3) 100)) (<= (+ (+ 25 xvar3) 75) (+ 175 xvar3))) :named named_assertion_2))
(assert (! (> xvar4 0) :named named_assertion_3))
(check-sat)
(get-model)

$ z3 namedtest.smt2 
sat
(
  (define-fun named_assertion_2 () Bool
    true)
  (define-fun named_assertion_3 () Bool
    (not (<= xvar4 0)))
  (define-fun named_assertion_1 () Bool
    (or (<= xvar2 (+ 75 xvar3))
    (>= xvar2 (+ 250 xvar3))
    (<= xvar1 (+ 50 xvar3))
    (>= xvar1 (+ 250 xvar4))))
  (define-fun xvar3 () Int
    0)
  (define-fun xvar1 () Int
    251)
  (define-fun xvar4 () Int
    1)
  (define-fun xvar2 () Int
    76)
)
$ cvc4 namedtest.smt2 
sat
(model
(define-fun xvar1 () Int 0)
(define-fun xvar2 () Int 0)
(define-fun xvar3 () Int 0)
(define-fun xvar4 () Int 1)
)
$ cvc5 namedtest.smt2 
sat
(
(define-fun xvar1 () Int 0)
(define-fun xvar2 () Int 0)
(define-fun xvar3 () Int 0)
(define-fun xvar4 () Int 1)
)
$ yices-smt2 --smt2-model-format namedtest.smt2 
sat
(model
  (define-fun xvar1 () Int 1)
  (define-fun xvar2 () Int 1)
  (define-fun xvar3 () Int 1)
  (define-fun xvar4 () Int 1))

Z3 version:

$ z3 --version
Z3 version 4.8.12 - 64 bit