Skip to content

Instantly share code, notes, and snippets.

@joelburget

joelburget/test.smt2

Created September 23, 2018 00:39
Show Gist options
  • Save joelburget/4223fea851fcfcd299aa76267aaab9fb to your computer and use it in GitHub Desktop.
Save joelburget/4223fea851fcfcd299aa76267aaab9fb to your computer and use it in GitHub Desktop.
Download ZIP
Raw
test.smt2
(set-logic ALL)
; define List
(declare-datatypes (T)
((List
(nil)
(cons (head T) (tail List)))))
; define len
(declare-fun len ((List Int)) Int)
(assert (forall ((xs (List Int)))
(= (len xs)
(ite (= xs nil) 0 (+ 1 (len (tail xs)))))))
(declare-const s0 Int)
(declare-const s1 Int)
(assert (= (len (cons s0 (cons s1 nil))) 2))
(check-sat)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment