Skip to content

Tutorial get-value example returns 8 instead of 6 #12

@kroeckx

Description

@kroeckx

The tutorial has this as example input:

(set-option :produce-models true)
(set-logic QF_LIA)
(declare-fun x () Int)
(declare-fun y () Int)
(assert (= (+ x y) 9))
(assert (= (+ (* 2 x) (* 3 y)) 22))
(check-sat)
(get-value (x))
(get-value ((- x y) (+ 2 y)))

And indicates this should be the output:

sat
((x 5))
(((- x y) 1)  ((+ 2 y) 8))

But either the 8 should be a 6, or the + a *

PS: I can't find the source of the tutorial

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type
    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions