Skip to content

fix: use asserting to model if without else#49

Merged
hargoniX merged 1 commit intomasterfrom
fix_sexp_model
Oct 30, 2025
Merged

fix: use asserting to model if without else#49
hargoniX merged 1 commit intomasterfrom
fix_sexp_model

Conversation

@hargoniX
Copy link
Member

This PR fixes the handling of non trivial if chains in sexpression model output. The key issue here
was the use of an if without else which is invalid syntax. Instead we use an asserting guard now.

Problematic part of the model before:

(if
 (and (= x_0 (l_BEq_elim__3_spec__18_mk $$anon_fun_0))
  (= x_1
   (l_List_elim__5_spec__16_cons
    $l___example_u945__8_elim__0_spec__15_0
    l_List_elim__5_spec__16_nil))
  (= x_2 l_List_elim__5_spec__16_nil) (= x_3 l_lt))
 l_Bool_elim__1_spec__13_false)

fixed part now:

(asserting l_Bool_elim__1_spec__13_false
  (and (= x_0 (l_BEq_elim__3_spec__18_mk $$anon_fun_0))
   (= x_1
    (l_List_elim__5_spec__16_cons
     $l___example_u945__8_elim__0_spec__15_0
     l_List_elim__5_spec__16_nil))
   (= x_2 l_List_elim__5_spec__16_nil) (= x_3 l_lt)))

Closes: #48

@hargoniX hargoniX merged commit 7de16b9 into master Oct 30, 2025
3 checks passed
@hargoniX hargoniX deleted the fix_sexp_model branch October 30, 2025 21:26
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Invalid Sexp model

1 participant