Satisfiability Modulo Theory (SMT) checking is concerned with checking the satisfiability of first-order formulas with respect to some background theories. The SMT-LIB format is a standardized language for scripts expressing SMT problems. Popular datasets of SMT-LIB scripts have been collected for benchmarking SMT solvers. Rather than focusing on evaluating SMT solvers, our work focuses on exploring how novice users write SMT-LIB scripts. We present a dataset of SMT-LIB scripts with fine-grained editing paths. The dataset consists of 2,415 editing paths with a total of 18,133 SMT-LIB scripts. All scripts were collected from a web-based interface for the Z3 SMT solver in educational settings. We analyze the dataset in terms of sizes of scripts, errors users make, similarities of consecutive scripts, editing distances, and edit steps required to fix errors. We make the dataset and the code for computing our metrics available for future research on language design, tool support, and teaching materials.
Satisfiability Modulo Theory (SMT) checking [
The SMT-LIB format is a standardized language [
Popular datasets of SMT-LIB scripts [
Thus, rather than focusing on evaluating SMT solvers, our work focuses on exploring how novice
users write SMT-LIB scripts. We present the FMPsmt dataset of SMT-LIB scripts with fine-grained editing
paths, i.e., sequences of SMT-LIB scripts that were consecutively written and analyzed by (novice)
users. The dataset consists of 2,415 editing paths with a total of 18,133 SMT-LIB scripts. All scripts were
collected from a web-based interface for the Z3 SMT solver [
We analyze the dataset in terms of sizes of scripts, errors users make, similarities of consecutive scripts,
editing distances, and edit steps required to fix errors. Our analyses are inspired by similar analyses
conducted on the aforementioned Alloy datasets [
The remainder of this work is structured as follows. Section 2 briefly presents the foundations of our work. Section 3 lists our research questions, Sect. 4 presents our dataset and data processing. Section 5 presents the evaluation of our research questions on the datasets. We conclude in Sect. 6.
We now give a brief overview of the SMT-LIB language specification and the Formal Methods Playground.
The SMT-LIB standard [
Listing 1: Excerpt of an example SMT-LIB script from the FMPsmt dataset
SMT-LIB scripts are sequences of commands, e.g., the set-logic command selecting the logic of uninterpreted functions in Listing 1, l. 1, the command assert for asserting formulas in Listing 1, ll. 9-15, or the command check-sat for checking satisfiability of the asserted formulas. Additional commands with prefix declare- introduce datatypes (Listing 1, l. 2), constants, and functions (Listing 1, ll. 3-6). The command get-model (Listing 1, ll. 17), if successful, retrieves an interpretation of constants and functions satisfying all asserted formulas and presents them as function definitions, e.g., the interpretation of constant Killer will be defined as the value Agatha, Butler, or Charles.
The Formal Methods Playground2 is a web application for writing and analyzing models, specifications,
and scripts in various modeling and specification languages. We have developed this application mainly
for teaching, e.g., slides in our Formal Methods for Software Engineering lecture [
We aim to gain a better understanding of how novice users write and evolve SMT-LIB scripts.
We define the following research questions: • RQ1: What are the key characteristics of the FMPsmt dataset? • RQ2: Where do users most commonly introduce syntactic errors in SMT-LIB scripts? • RQ3: How do consecutive SMT-LIB scripts difer? • RQ4: How large are the edit distances between consecutive SMT-LIB scripts? • RQ5: How do users fix errors over multiple edit steps?
We analyze our proposed Formal Methods Playground SMT-LIB (FMPsmt) dataset [
The FMPsmt datasets maintain records of the previous revision of each SMT script. Each revision is a user submission i.e., the current script whenever the user executes the solver. We utilize this information to reconstruct the edit path4, allowing us to capture the sequences of edits/submissions made by users (these edits are typically small, see Sect. 5.4).
The FMPsmt dataset consists of 2,415 unique edit paths. In particular, the top 25% of the edit paths have a length greater than 13 for FMPsmt, with median lengths of 6. The FMPsmt dataset has 272 unique initial scripts5 within the edit paths.
Note that the number of scripts in edit paths exceeds the total number of scripts in the dataset. The exchange of permalinks to individual scripts via the Formal Methods Playground allows the branching of edit paths leading to common prefixes.
Q3
For semantic comparison, we utilize a lightweight procedure (implemented using Z3 [
It is important to note that this semantic comparison approach is naive and has several limitations. The comparison is oblivious to variable renaming, ignores push and pop scopes, and can misclassify scripts that contain inconsistent or unsatisfiable assertions. Consequently, the reported relationships are approximate and may not accurately reflect subtle semantic nuances. However, relatively small edit distances (see Sect. 5.4), i.e., syntactically very similar scripts in edit paths, and low numbers of incremental scripts (see Sect. 5.1) suggest a potential for the analysis on the FMPsmt dataset.
We now present data to answer our research questions from Sect. 3. All experiments used Z3 v4.13.4 and were executed on a server with an Intel Xeon Platinum 8260 CPU @ 2.4GHz running Ubuntu 22.04.
To characterize the FMPsmt dataset, we conducted a quantitative analysis based on several structural and syntactic features. These include efective lines of code (ELOC), the frequency of common SMT-LIB commands such as assert, declare-const, check-sat, etc., as well as the maximum nesting depth of expressions within each script.
Table 1a summarizes the distribution of key structural features in the FMPsmt dataset, highlighting 25th percentile, median, 75th percentile, and maximum values. Efective lines of code (ELOC) have a median of 26 and a maximum of 1,531, indicating most scripts are small, but a few are much larger. The maximum nesting depth of operators is generally low, with a median maximum nesting depth of 5, with some outliers reaching 42, suggesting instances of highly nested formulas. The counts of diferent commands per script increase with ELOC.
The FMPsmt dataset comprises 1,221 (6.73%) scripts with multiple check-sat commands (incremental
scripts in the terminology of the SMT-LIB benchmark [
The dataset spans a wide range of SMT logics—38 in total (including typos)—with QF_UF (1,819 scripts), QF_LIA (1,447 scripts), and QF_AUFLIA (401 scripts) being the most common. Note that many scripts do not declare a logic, as Z3 does not enforce this. Less frequent logics include specialized or rarely used ones, such as QF_SLIA, appearing only once. This variety emphasizes the dataset’s extensive scope, encompassing both quantifier-free and quantified fragments. 50.46% 65.26% 32.92%
Edit Paths (100%) With Invalid Scripts (%) Without Valid Scripts (%) (b)
#
Table 1b summarizes the distribution of edit path lengths. The dataset comprises 2,415 distinct edit paths, with lengths from 1 to 321 edits. The median length is 6, and the 75th percentile is 13, suggesting that while some users finish their analyses quickly, many engage in longer editing processes. Notably, over 58% of edit paths have five or more steps, highlighting the significant time and efort users invest in refining their scripts.
We also investigated the frequency with which users encounter syntactic errors in these paths. Table 2b shows that 59.13% of edit paths contain at least one invalid script, suggesting users often make erroneous iterations before reaching a correct version. Only 1.41% of paths consist entirely of invalid scripts, indicating instances where users cannot construct a syntactically valid SMT-LIB script.
Another important characteristic of the dataset is the degree of syntactic uniqueness across scripts. As shown in Table 2a, 9150 scripts (50.46%) are syntactically unique, indicating that more than half of the dataset comprises distinct SMT-LIB formulations rather than duplicates or near-duplicates. Among these unique scripts, 5971 (65.26%) are syntactically correct, highlighting a reasonably high rate of well-formed inputs within the diverse subset.
In summary, the FMPsmt dataset consists of SMT-LIB scripts of mainly small to medium sizes (median 26 ELOC) and complexities, encompassing a broad range of 38 diferent logics (including typos). The execution times are typically brief (within tens of milliseconds), and users often refine scripts iteratively. The dataset includes a wide range of problem instances, as well as diverse modeling styles and patterns.
Among the 18,133 SMT-LIB scripts analyzed within the FMPsmt dataset, we observed that approximately 40% contain at least one syntax error, which is distributed across various SMT commands. To analyze common syntactic errors in SMT-LIB scripts, we developed a parser to identify and categorize errors. For each identified syntactic error, we recorded the top-level SMT-LIB command, the absolute number of errors, the total occurrences of the command, and calculated the relative percentage of errors for each command.
Table 3 presents the ten commands most susceptible to user-induced syntactic errors, evaluated by both absolute and relative frequencies of errors. The assert command accounts for the highest absolute number of errors, with 35,132 instances (11.01%), likely due to the inherent complexity of the logical expressions it often encompasses. In contrast, the declare-const command shows 10,920 errors, but with a lower error rate of 4.85%, indicating that it is mostly used correctly despite its frequent use. Interestingly, the commands get-value and eval exhibit the highest relative error rates, at 30.62% and 27.96%, respectively. These commands are less common but appear to be more error-prone. However, command assert declare-const declare-fun get-value define-fun get-model declare-datatype check-sat eval quantifiers
abs. # error # total elements rel. % of command note that our automated analyses of errors in SMT-LIB scripts did not distinguish between static syntax errors, e.g., invoking command get-value for an undeclared constant, and runtime errors, e.g., invoking command get-value without a model. We leave a more detailed investigation to future work.
The absolute and relative numbers of errors in Table 3 suggest that while assert is frequently used and therefore contributes a large raw number of errors, commands like get-value and eval might proportionally be more challenging for novice users to implement correctly.
Building on the analysis of error distribution across SMT-LIB commands, we investigated the specific
types of syntactic errors encountered by users. Table 4 summarizes the top 10 categories of syntactic
errors observed in the FMPsmt dataset. These errors are classified according to frequent patterns
observed in the error messages. Detailed information regarding the exact and complete error messages
for each script6 can be found in the replication package [
The most prevalent error, accounting for over 50% of all cases, is "Unknown constant", which typically arises when users reference symbols that have not been previously declared. This suggests a recurring issue with undeclared variables or scope-related oversights in SMT-LIB scripts. The following most common categories involve incorrect or malformed declarations, such as "Invalid constant declaration" (9.8%) and "Parsing function declaration" errors (7.16%), indicating that sort mismatches and incorrect syntactic forms in declarations are also significant sources of failure.
These errors highlight a common challenge that novice users encounter with sort declarations and
naming conventions in SMT-LIB. Many of these issues are avoidable and could likely be minimized
through improved language support, such as context-aware autocompletion, scoping, referencing,
validation, and informative diagnostics that guide users toward correct usage as they write. Partially,
these analyses are already supported by existing tools, e.g., Dolmen [
Errors such as "Logic does not support" and "Model is not available" indicate issues related to the selected logic or solver state. If the commands are misused in a given context, these issues can also appear as syntactic problems.
In summary, syntactic errors in the FMPsmt dataset (mainly referencing unknown constants or writing invalid declarations) are both frequent and concentrated around specific SMT-LIB commands and constructs (mainly in assertions and declarations). Common errors include malformed or mismatched declarations, pointing to challenges in understanding SMT-LIB’s type and declaration system. These insights suggest a need for improved tooling and guidance, such as contextual validation, better scoping support, and more intelligent error detection and error messages to assist users. 6See file https://raw.githubusercontent.com/se-buw/smt-metrics/refs/tags/SMT2025/results/fmp_error_category.csv
To understand the evolution of SMT-LIB scripts during user editing sessions, we analyzed the diferences between “consecutive” (i.e., directly successive) and “non-consecutive” (i.e., scripts related through longer edit paths) script pairs along each edit path (see Sect. 4.2). Our analysis addresses both syntactic identity and various semantic relationships, including equivalence (≡ ), incomparability (̸=), and refinement relationships (1 ⊏ 2 and 2 ⊏ 1) as mentioned in Sect. 4.3.
As shown in Table 5, a substantial number of consecutive script pairs (4,319 pairs) were syntactically identical, which is significantly higher than for non-consecutive pairs (2,121 pairs). This suggests users often submit the same script without modifications, e.g., when reviewing their own earlier work or examples provided in permalinks.
This analysis revealed that only 23.86% of consecutive script pairs (6,332 pairs) in the edit paths are semantically equivalent, while over 10% (2,805 pairs) are incomparable, and roughly 11% (1,149 and 1,748 pairs) exhibit refinement relations. This indicates significant changes in specification behavior, even among consecutive edits. Furthermore, we have identified 216 unknowns. Note that these percentages do not add up to 100% as one syntactically incorrect script in a pair prevents our semantic comparison of that pair.
In contrast, non-consecutive script pairs on the same edit path demonstrate lower semantic equivalence (8.04%) but higher rates of incomparability (19.48%). These trends suggest that as users make more edits over time, scripts tend to diverge semantically, reflecting an increasing complexity in the SMT script. Interestingly, refinement relationships remain prevalent even in non-consecutive pairs, implying that users incrementally strengthen or weaken specifications throughout the editing process.
As an example, Listings 2 and 3 demonstrate a refinement relation between two SMT-LIB scripts. Listing 2 has a stronger specification that creates a cyclic chain of Boolean implications leading to a contradiction. Conversely, Listing 3 asserts a weaker property that is always satisfiable. Our semantic comparison reveals that Listing 2 ⊏ Listing 3: all models of the listing 2 (none, in this case) satisfy the assertions in Listing 3, but not vice versa.
In summary, over 4,300 consecutive pairs are syntactically identical, indicating user habits, such as rerunning unchanged scripts. Consecutive scripts show high numbers of cases of semantic equivalence and refinement, implying that users refine their logic incrementally. The persistence of refinement in both consecutive and non-consecutive pairs highlights a frequent pattern of strengthening or weakening specifications, suggesting a trial-and-error process in developing SMT scripts.
To explore the evolution of SMT-LIB scripts across edit paths, we calculate the Levenshtein distance [
The findings are summarized in Table 6, illustrating that most script edits tend to be minor. The 25th percentile of edit distances is 6, while the median stands at 51, suggesting that users implement only slight adjustments between successive versions in over half of the instances. These adjustments can involve minor tweaks such as refining logical assertions, correcting constants, adding or removing a single command, or fixing formatting issues.
Nonetheless, the distribution shows a lengthy tail of significant edits. The 75th percentile sits at 315 characters, while the maximum distance reaches 38,659, indicating infrequent yet significant rewrites. These large distances correspond to major structural changes or cases where the user replaces the existing script entirely, potentially because they are starting anew. In summary, the edit distances between consecutive SMT-LIB scripts indicate that the majority of user edits are small (median 51 characters). This suggests that users generally implement incremental adjustments such as refining assertions, correcting errors, or modifying individual commands– rather than undertaking comprehensive overhauls of entire scripts.
Our analysis indicates that approximately 40% of all scripts exhibit at least one syntax error (see Sect. 5.1), while approximately 60% of the edit paths are characterized by the presence of at least one erroneous script (see Table 1b).
To quantify the efort required for error resolution, we calculated the number of consecutive edit steps necessary to rectify specific types of issues. Table 7 presents the quartiles and maximum values for the steps involved in correcting syntax errors and transforming an unsatisfiable (UNSAT) script into a satisfiable (SAT) script.
The data indicates that most syntax errors are corrected swiftly: both the 25th percentile (Q1) and the median stand at 1, meaning that in at least half of the instances, users address a parse error in just one edit step. The 75th percentile (Q3) is 3, whereas the most prolonged fix recorded took 52 edit steps. This suggests that while fast recovery is typical, some users face considerable challenges, particularly with longer or more intricate scripts.
Similarly, the process of resolving semantic unsatisfiability, which involves changing a script from UNSAT to SAT, also demonstrates a high degree of eficiency. The median number of steps required is 1, with 75% of transitions occurring within two steps. This suggests that users often make precise logical adjustments in a single step once they recognize unsatisfiability. However, some complex semantic issues resulted in up to 58 steps for correction.
These findings indicate that novice users are typically able to address syntactical issues and advance towards satisfiability with low efort; however, they also underscore the existence of non-trivial challenges in a minority of instances.
In summary, most users resolve syntax and satisfiability issues quickly, often within a single edit. This indicates users typically identify and fix problems with minimal efort. However, some cases require extensive revisions, highlighting that, while rapid recovery is common, some users face significant challenges with complex debugging tasks.
We now identify and discuss various threats to the validity of our analyses. For transparency and
reproducibility we provide the implementation of our processing in [
First, we assume that the use of the Formal Methods Playground across the dataset is similar to that of our students, i.e., small models are created and analyzed. However, we have no control over how other users use the publicly available platform, e.g., it could be used for teaching with very narrow task definitions. To assess this uncertainty, we have assessed unique initial nodes of edit paths in Sect. 4.2, giving some confidence in the models’ variability.
Second, the permalinks provided in the lecture materials might have inadvertently encouraged users to begin their models from these pre-existing structures. This could afect the root nodes of edit paths, complicating the comparison of model evolution across various initial states and potentially underestimating the diversity of evolution paths. Additionally, users may forget to reset the edit path after completing one model and before starting another, i.e., the edit paths of the new model may incorrectly link to the previous one. This could distort the sequence of changes and hinder our ability to analyze the edit paths accurately.
Third, the dataset captures only a small portion of the SMT-LIB standard and is primarily written by novice users introduced to SMT-LIB through lecture materials. Any findings are restricted to these assumptions and may not be generalized. In particular, while it might seem surprising that unsatisfiability is often resolved in a single edit step, this could be due to the prevalence of small SMT scripts with few assertions.
We have presented and analyzed the Formal Methods Playground SMT-LIB (FMPsmt) dataset. We analyzed the dataset in terms of sizes of scripts, errors users make, syntactic and semantic similarity of consecutive scripts, editing distances, and edit steps required to fix errors. Syntactic errors are highly prevalent in writing SMT-LIB scripts, and our analysis reveals common syntax error classes that could likely be avoided with improved tool support, such as code completion and reference and scope checking. Interestingly, debugging unsatisfiability did not appear to present a problem to users, and scripts returned to being satisfiable often within a single editing step.
We have made the Formal Methods Playground SMT-LIB (FMPsmt) dataset publicly available on Zenodo
as [
We want to acknowledge Salar Kalantari’s MSc thesis [