1 2 3 4 5 6 7 8 9 10
; COMMAND-LINE: --sygus-inst --strings-exp --no-check-models ; EXPECT: sat (set-logic NIA) (set-option :sygus-inst true) (set-option :strings-exp true) (set-info :status sat) (declare-fun d () Int) (assert (forall ((g Int)) (or (> 1 g) (> g (div 1 d))))) (assert (not (= d 0))) (check-sat)