Skip to content

z3 reports invalid model  #2676

@muchang

Description

@muchang

Hi,
For this formula,

(declare-fun a () Int)
(declare-fun b () Bool)
(declare-fun c () Bool)
(declare-fun d () Bool)
(declare-fun e () Bool)
(assert (= b (= (/ 1 0) a) (= b d e) (= e c d)))
(check-sat)
(get-model)

z3 will report a invaild model:

(model 
  (define-fun e () Bool
    true)
  (define-fun c () Bool
    false)
  (define-fun d () Bool
    true)
  (define-fun a () Int
    0)
  (define-fun b () Bool
    true)
)

OS: Ubuntu 18.04
Revision: 16d4ccd

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions