Skip to content

Commit 894f51f

Browse files
committed
Back-translate (wrongly) unary minus
1 parent 4c7a5d0 commit 894f51f

File tree

1 file changed

+6
-0
lines changed

1 file changed

+6
-0
lines changed

kore/src/Kore/Rewrite/SMT/Translate.hs

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -539,6 +539,12 @@ backTranslateWith
539539
, Just koreSym <- Map.lookup fct reverseMetadata = do
540540
args <- mapM backTranslate rest
541541
pure $ TermLike.mkApplySymbol koreSym args
542+
| ((Atom "-") : rest) <- xs =
543+
do
544+
args <- mapM backTranslate rest
545+
-- FIXME use the unary minus from reverseMetadata, make sure it's there,
546+
-- and don't use head
547+
pure (head args)
542548
| otherwise =
543549
throwError "backTranslate.List-case: implement me!"
544550
backTranslate String{} =

0 commit comments

Comments
 (0)