definitions.smt2

(set-logic QF_SLIA) ;; Changed logic to String flow (Strings, Linear Integer Arithmetic)

;; ------------------------------------------------------------
;; DEFINITIONS: Shared Schema and Constants
;; ------------------------------------------------------------

;; 1. String Constants (Now defined as actual String literals)
;; This is what you were looking for!
(define-const STR_INSERT_OR_UPDATE String "INSERT_OR_UPDATE")
(define-const STR_SYS_WS_OPERATION String "sys_ws_operation")
(define-const STR_OTHER String "other")

;; 2. Schema Variables (Update Set Metadata)
;; Now these are of type 'String' (built-in SMT type)
(declare-fun Action () String)
(declare-fun Table () String)

;; 3. Schema Variables (Taint Analysis - Bool remains the same)
(declare-const script_source_is_user_input Bool)
(declare-const script_sink_is_dangerous Bool)
(declare-const script_flow_exists Bool)