Skip to content

Instantly share code, notes, and snippets.

@KevinKu
Created November 5, 2017 09:30
Show Gist options
  • Save KevinKu/58416f46dc4ba3421591065471722740 to your computer and use it in GitHub Desktop.
Save KevinKu/58416f46dc4ba3421591065471722740 to your computer and use it in GitHub Desktop.
(declare-const x0 Int)
(declare-const x1 Int)
(declare-const x2 Int)
(assert(and (and (or (< x0 10) (= x0 10)) (= x1 (- x0 1))) (and (= x2 x1) (= x2 9) ) ))
(check-sat)
output:sat
(declare-const x0 Int)
(declare-const x1 Int)
(declare-const x2 Int)
(assert(and (> x0 10) (and (= x2 x0) (= x2 9) ) ))
(check-sat)
output:unsat
所以是整個logic formula是滿足的 , 代表有個int value會使執行時出現assert的錯誤訊息
就是x=10的時候
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment