[Question][Hw2] On grading the counterexamples in program equivalence checker

[jaehyun1ee]

Hi, I have one question regarding the grading method of eq in our homework assignment.

When two programs, src and tgt are not functionally equivalent, our program should print satisfiable, with a counterexample. (Counterexample that makes the two programs return different output for the same input)

I wonder if the homework grader will take into account that there may be multiple counterexamples for satisfiable case.

To illustrate, for test/eq3.scm,

; f(x) = let y = 1 in if (x = y) then 1 else y
(let y 1 (if (= x y) 1 1))
; f(x) = x
x

the expected output in the given repository is,

satisfiable
(define-fun tgt_x () Int
  2)
(define-fun src_x () Int
  2)
(define-fun src_y () Int
  1)

But my program gives,

satisfiable
(define-fun src_y () Int
  1)
(define-fun tgt_x () Int
  0)
(define-fun src_x () Int
  0)

So the CI workflow in my homework repository fails. However, I believe my output is also acceptable. There can be many counterexamples, and I wonder if the grader of this assignment will take this into consideration.

Thank you in advance :)

[Hhro]

Hi,

If the judgment on satisfiability is correct and the counter-example(if it exists) is proper, then, surely, you would obtain the score. So, don't worry!

Thanks.

[jaehyun1ee]

Thank you for the kind answer :)