Skip to content

Commit

Permalink
Fix evaluator for prefixof in Eunoia (cvc5#11419)
Browse files Browse the repository at this point in the history
  • Loading branch information
ajreynol authored Dec 6, 2024

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature. The key has expired.
1 parent 1d50fb8 commit 4d8c080
Showing 3 changed files with 9 additions and 1 deletion.
2 changes: 1 addition & 1 deletion proofs/eo/cpc/Cpc.eo
Original file line number Diff line number Diff line change
@@ -163,7 +163,7 @@
))))
(($run_evaluate (str.prefixof x y)) (eo::define ((ex ($run_evaluate x)))
(eo::define ((ey ($run_evaluate y)))
(eo::define ((r (eo::find ex ey)))
(eo::define ((r (eo::find ey ex)))
(eo::ite (eo::is_eq r 0) true
(eo::ite (eo::is_z r) false
(str.prefixof ex ey)))))))
1 change: 1 addition & 0 deletions test/regress/cli/CMakeLists.txt
Original file line number Diff line number Diff line change
@@ -1348,6 +1348,7 @@ set(regress_0_tests
regress0/proofs/lfsc-test-1.smt2
regress0/proofs/nomerge-alethe-pf.smt2
regress0/proofs/no-proof-uc.smt2
regress0/proofs/pfcheck_rw_441.smt2
regress0/proofs/pp-only-proof.smt2
regress0/proofs/open-pf-datatypes.smt2
regress0/proofs/open-pf-if-unordered-iff.smt2
7 changes: 7 additions & 0 deletions test/regress/cli/regress0/proofs/pfcheck_rw_441.smt2
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
; EXPECT: unsat
(set-logic QF_SLIA)
(declare-fun x () String)
(declare-fun y () String)
(declare-fun z () Int)
(assert (not (= (str.prefixof "B" (str.substr x z 0)) false)))
(check-sat)

0 comments on commit 4d8c080

Please sign in to comment.